let X1, X2 be set ; :: thesis: ( ( for x being object holds
( x in X1 iff x = y ) ) & ( for x being object holds
( x in X2 iff x = y ) ) implies X1 = X2 )
assume that
A1: for z being object holds
( z in X1 iff z = y ) and
A2: for z being object holds
( z in X2 iff z = y ) ; :: thesis: X1 = X2

now :: thesis: for z being object holds
( z in X1 iff z in X2 )

let z be object ; :: thesis: ( z in X1 iff z in X2 )
( z in X1 iff z = y ) by A1;
hence ( z in X1 iff z in X2 ) by A2; :: thesis: verum

end;

hence X1 = X2 by TARSKI_0:2; :: thesis: verum