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

proof

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

end;

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

proof

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

end;

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