let x be object ; TARSKI:def 3 ( not x in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } or x in { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } )
assume
x in { F3(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : P1[u9,v9] }
; x in { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
then consider u being Element of F1(), v being Element of F2() such that
A2:
x = F3(u,v)
and
A3:
P1[u,v]
;
P2[u,v]
by A1, A3;
hence
x in { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
by A2; verum