let A, B be set ; :: thesis: ( ( for z being set st z in A holds
ex x, y being set st z = [x,y] ) & ( for z being set st z in B holds
ex x, y being set st z = [x,y] ) & ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) implies A = B )
assume that
A1: for z being set st z in A holds
ex x, y being set st z = [x,y] and
A2: for z being set st z in B holds
ex x, y being set st z = [x,y] and
A3: for x, y being set holds
( [x,y] in A iff [x,y] in B ) ; :: thesis: A = B

now

let z be set ; :: thesis: ( z in A iff z in B )
A4: ( z in B implies ex x, y being set st z = [x,y] ) by A2;
( z in A implies ex x, y being set st z = [x,y] ) by A1;
hence ( z in A iff z in B ) by A3, A4; :: thesis: verum

end;

hence A = B by TARSKI:2; :: thesis: verum