theorem :: TARSKI:2

for X, Y being set st ( for x being object holds
( x in X iff x in Y ) ) holds
X = Y by TARSKI_0:2;