set Z = { F₂(z) where z is Element of F₁() : P₁[z] } ;
set X = { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } ;
A0: union { F₂(z) where z is Element of F₁() : P₁[z] } c= union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { F₂(z) where z is Element of F₁() : P₁[z] } or x in union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } )
assume x in union { F₂(z) where z is Element of F₁() : P₁[z] } ; :: thesis: x in union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] }
then consider Y being set such that
A3: ( x in Y & Y in { F₂(z) where z is Element of F₁() : P₁[z] } ) by TARSKI:def 4;
consider z being Element of F₁() such that
A4: ( Y = F₂(z) & P₁[z] ) by A3;
Y c= varcl Y by VARCL;
then ( varcl Y in { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } & x in varcl Y ) by A3, A4;
hence x in union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } by TARSKI:def 4; :: thesis: verum

end;

now

let x, y be set ; :: thesis: ( [x,y] in union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } implies x c= union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } )
assume [x,y] in union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } ; :: thesis: x c= union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] }
then consider Y being set such that
A1: ( [x,y] in Y & Y in { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } ) by TARSKI:def 4;
consider z being Element of F₁() such that
A2: ( Y = varcl F₂(z) & P₁[z] ) by A1;
( x c= Y & Y c= union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } ) by A1, A2, VARCL, ZFMISC_1:92;
hence x c= union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } by XBOOLE_1:1; :: thesis: verum

end;

hence varcl (union { F₂(z) where z is Element of F₁() : P₁[z] } ) c= union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } by A0, VARCL; :: according to XBOOLE_0:def 10 :: thesis: union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } c= varcl (union { F₂(z) where z is Element of F₁() : P₁[z] } )
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } or x in varcl (union { F₂(z) where z is Element of F₁() : P₁[z] } ) )
assume x in union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } ; :: thesis: x in varcl (union { F₂(z) where z is Element of F₁() : P₁[z] } )
then consider Y being set such that
A4: ( x in Y & Y in { (varcl F₂(z)) where z is Element of F₁() : P₁[z] } ) by TARSKI:def 4;
consider z being Element of F₁() such that
A5: ( Y = varcl F₂(z) & P₁[z] ) by A4;
F₂(z) in { F₂(z) where z is Element of F₁() : P₁[z] } by A5;
then Y c= varcl (union { F₂(z) where z is Element of F₁() : P₁[z] } ) by A5, Th13, ZFMISC_1:92;
hence x in varcl (union { F₂(z) where z is Element of F₁() : P₁[z] } ) by A4; :: thesis: verum