set A = { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } ;
set C = { F₄(u3,v3) where u3 is Element of F₁(), v3 is Element of F₂() : P₁[u3,v3] } ;
for a being object holds
( a in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } iff a in { F₄(u3,v3) where u3 is Element of F₁(), v3 is Element of F₂() : P₁[u3,v3] } )

proof

let a be object ; :: thesis: ( a in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } iff a in { F₄(u3,v3) where u3 is Element of F₁(), v3 is Element of F₂() : P₁[u3,v3] } )

hereby :: thesis: ( a in { F₄(u3,v3) where u3 is Element of F₁(), v3 is Element of F₂() : P₁[u3,v3] } implies a in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } )

assume a in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } ; :: thesis: a in { F₄(u3,v3) where u3 is Element of F₁(), v3 is Element of F₂() : P₁[u3,v3] }
then consider u being Element of F₁(), v being Element of F₂() such that
A2: a = F₃(u,v) and
A3: P₁[u,v] ;
a = F₄(u,v) by A1, A2, A3;
hence a in { F₄(u3,v3) where u3 is Element of F₁(), v3 is Element of F₂() : P₁[u3,v3] } by A3; :: thesis: verum

end;

assume a in { F₄(u3,v3) where u3 is Element of F₁(), v3 is Element of F₂() : P₁[u3,v3] } ; :: thesis: a in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] }
then consider u being Element of F₁(), v being Element of F₂() such that
A4: a = F₄(u,v) and
A5: P₁[u,v] ;
a = F₃(u,v) by A1, A4, A5;
hence a in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } by A5; :: 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 TARSKI:2; :: thesis: verum