let x, y be object ; for x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
let x1, y1 be set ; ( [x,y] in {[x1,y1]} implies ( x = x1 & y = y1 ) )
assume
[x,y] in {[x1,y1]}
; ( x = x1 & y = y1 )
then
[x,y] = [x1,y1]
by TARSKI:def 1;
hence
( x = x1 & y = y1 )
by XTUPLE_0:1; verum