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

now

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

end;

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