axiom prop_ext: !P:prop.!Q:prop.(P <-> Q) -> P = Q axiom func_ext: !p:set prop.!q:set prop.(!x:set.p x = q x) -> p = q claim !p:set prop.!q:set prop.(!x:set.p x <-> q x) -> p = q