set Y = { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] } ;
set X = { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } ;
A2: { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] } c= { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] } or x in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } )
assume x in { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] } ; :: thesis: x in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] }
then consider u1 being Element of F₁(), v1 being Element of F₂() such that
A3: x = F₄(u1,v1) and
A4: P₁[u1,v1] ;
x = F₃(u1,v1) by A1, A3;
hence x in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } by A4; :: thesis: verum

end;

{ F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } c= { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } or x in { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] } )
assume x in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } ; :: thesis: x in { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] }
then consider u1 being Element of F₁(), v1 being Element of F₂() such that
A5: x = F₃(u1,v1) and
A6: P₁[u1,v1] ;
x = F₄(u1,v1) by A1, A5;
hence x in { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] } by A6; :: thesis: verum

end;

hence { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } = { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] } by A2; :: thesis: verum