let x, y be object ; :: thesis: for X, Y being set st Y in swap (X,x,y) & x <> y & not y in union X holds
( x in Y iff not y in Y )
let X, Y be set ; :: thesis: ( Y in swap (X,x,y) & x <> y & not y in union X implies ( x in Y iff not y in Y ) )
assume A1: ( Y in swap (X,x,y) & x <> y & not y in union X ) ; :: thesis: ( x in Y iff not y in Y )

per cases then ( Y in { ((A \ {x}) \/ {y}) where A is Element of X : x in A } or Y in { (A \/ {x}) where A is Element of X : ( not x in A & A in X ) } ) by XBOOLE_0:def 3;

suppose Y in { ((A \ {x}) \/ {y}) where A is Element of X : x in A } ; :: thesis: ( x in Y iff not y in Y )

then consider A being Element of X such that
A2: ( Y = (A \ {x}) \/ {y} & x in A ) ;

hereby :: thesis: ( not y in Y implies x in Y )

assume x in Y ; :: thesis: not y in Y
then x in A \ {x} by A2, ZFMISC_1:136, A1;
hence not y in Y by ZFMISC_1:56; :: thesis: verum

end;

thus ( not y in Y implies x in Y ) by A2, ZFMISC_1:136; :: thesis: verum

end;

suppose Y in { (A \/ {x}) where A is Element of X : ( not x in A & A in X ) } ; :: thesis: ( x in Y iff not y in Y )

then consider A being Element of X such that
A3: ( Y = A \/ {x} & not x in A & A in X ) ;
not y in A by A1, A3, TARSKI:def 4;
hence ( x in Y iff not y in Y ) by A3, ZFMISC_1:136, A1; :: thesis: verum

end;

end;