let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F2(v9) where v9 is Element of F1() : P1[v9] } or x in { F2(u9) where u9 is Element of F1() : P2[u9] } )
assume x in { F2(v9) where v9 is Element of F1() : P1[v9] } ; :: thesis: x in { F2(u9) where u9 is Element of F1() : P2[u9] }
then consider v being Element of F1() such that
A2: x = F2(v) and
A3: P1[v] ;
 P2[v] by A1, A3;
hence x in { F2(u9) where u9 is Element of F1() : P2[u9] } by A2; :: thesis: verum