const In : set set prop term iIn = In infix iIn 2000 2000 term PNoEq_ = \x:set.\p:set prop.\q:set prop.!y:set.y iIn x -> (p y <-> q y) axiom iff_sym: !P:prop.!Q:prop.(P <-> Q) -> (Q <-> P) claim !x:set.!p:set prop.!q:set prop.PNoEq_ x p q -> !y:set.y iIn x -> (q y <-> p y)