defpred S1[ set ] means ( P2[$1] & P1[$1] );
defpred S2[ set ] means ( $1 in { s1 where s1 is Element of F1() : P2[s1] } & P1[$1] );
A1:
for s being Element of F1() holds
( S2[s] iff S1[s] )
proof
let s be
Element of
F1();
( S2[s] iff S1[s] )
now ( s in { s1 where s1 is Element of F1() : P2[s1] } implies P2[s] )assume
s in { s1 where s1 is Element of F1() : P2[s1] }
;
P2[s]then
ex
s1 being
Element of
F1() st
(
s = s1 &
P2[
s1] )
;
hence
P2[
s]
;
verum end;
hence
(
S2[
s] iff
S1[
s] )
;
verum
end;
thus
{ F2(s) where s is Element of F1() : S2[s] } = { F2(s2) where s2 is Element of F1() : S1[s2] }
from FRAENKEL:sch 3(A1); verum