let X1, X2 be set ; ( ( for x being object holds
( x in X1 iff ex Y being set st
( x in Y & Y in X ) ) ) & ( for x being object holds
( x in X2 iff ex Y being set st
( x in Y & Y in X ) ) ) implies X1 = X2 )
assume that
A1:
for x being object holds
( x in X1 iff ex Y being set st
( x in Y & Y in X ) )
and
A2:
for x being object holds
( x in X2 iff ex Y being set st
( x in Y & Y in X ) )
; X1 = X2
now for x being object holds
( x in X1 iff x in X2 )let x be
object ;
( x in X1 iff x in X2 )
(
x in X1 iff ex
Y being
set st
(
x in Y &
Y in X ) )
by A1;
hence
(
x in X1 iff
x in X2 )
by A2;
verum end;
hence
X1 = X2
by TARSKI_0:2; verum