defpred S₁[ set ] means ( $1 in { s1 where s1 is Element of F₁() : P₂[s1] } & P₁[$1] );
defpred S₂[ set ] means ( P₂[$1] & P₁[$1] );
A1: for s being Element of F₁() holds
( S₁[s] iff S₂[s] )

proof

let s be Element of F₁(); :: thesis: ( S₁[s] iff S₂[s] )

now

assume s in { s1 where s1 is Element of F₁() : P₂[s1] } ; :: thesis: P₂[s]
then ex s1 being Element of F₁() st
( s = s1 & P₂[s1] ) ;
hence P₂[s] ; :: thesis: verum

end;

hence ( S₁[s] iff S₂[s] ) ; :: thesis: verum

end;

thus { F₂(s) where s is Element of F₁() : S₁[s] } = { F₂(s2) where s2 is Element of F₁() : S₂[s2] } from FRAENKEL:sch 3(A1); :: thesis: verum