set A = { o where o is Element of F₁() : P₁[o] } ;

now

let x be set ; :: thesis: ( ( x in { o where o is Element of F₁() : P₁[o] } implies ex y being set st [x,y] in F₂() ) & ( ex y being set st [x,y] in F₂() implies x in { o where o is Element of F₁() : P₁[o] } ) )

hereby :: thesis: ( ex y being set st [x,y] in F₂() implies x in { o where o is Element of F₁() : P₁[o] } )

assume x in { o where o is Element of F₁() : P₁[o] } ; :: thesis: ex y being set st [x,y] in F₂()
then consider o being Element of F₁() such that
A2: x = o and
A3: P₁[o] ;
take y = F₃(o); :: thesis: [x,y] in F₂()
thus [x,y] in F₂() by A1, A2, A3; :: thesis: verum

end;

given y being set such that A4: [x,y] in F₂() ; :: thesis: x in { o where o is Element of F₁() : P₁[o] }
consider o being Element of F₁() such that
A5: [x,y] = [o,F₃(o)] and
A6: P₁[o] by A1, A4;
x = o by A5, ZFMISC_1:33;
hence x in { o where o is Element of F₁() : P₁[o] } by A6; :: thesis: verum

end;

hence dom F₂() = { o where o is Element of F₁() : P₁[o] } by RELAT_1:def 4; :: thesis: verum