let p1, p2 be set ; :: thesis: ( ( for z being set holds
( z in p1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) & ( for z being set holds
( z in p2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) implies p1 = p2 )
assume that
A4: for z being set holds
( z in p1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) and
A5: for z being set holds
( z in p2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ; :: thesis: p1 = p2

now

let z be set ; :: thesis: ( z in p1 iff z in p2 )
( z in p1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) by A4;
hence ( z in p1 iff z in p2 ) by A5; :: thesis: verum

end;

hence p1 = p2 by TARSKI:2; :: thesis: verum