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) term nIn = \x:set.\y:set.~ x iIn y axiom In_irref: !x:set.nIn x x axiom iffI: !P:prop.!Q:prop.(P -> Q) -> (Q -> P) -> (P <-> Q) claim !x:set.!p:set prop.!y:set.y iIn x -> (p y <-> p y & y != x)