let M1, M2 be non empty set ; :: thesis: ( M1 <==> M2 iff for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) )
thus ( M1 <==> M2 implies for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) ) :: thesis: ( ( for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) ) implies M1 <==> M2 )

proof

assume A1: for H being ZF-formula st Free H = {} holds
( M1 |= H iff M2 |= H ) ; :: according to ZFREFLE1:def 2 :: thesis: for F being Subset of WFF holds
( M1 |= F iff M2 |= F )
let F be Subset of WFF; :: thesis: ( M1 |= F iff M2 |= F )
thus ( M1 |= F implies M2 |= F ) :: thesis: ( M2 |= F implies M1 |= F )

proof

assume A2: for H being ZF-formula st H in F holds
M1 |= H ; :: according to ZFREFLE1:def 1 :: thesis: M2 |= F
let H be ZF-formula; :: according to ZFREFLE1:def 1 :: thesis: ( H in F implies M2 |= H )
consider S being ZF-formula such that
A3: Free S = {} and
A4: for M being non empty set holds
( M |= S iff M |= H ) by Th6;
assume H in F ; :: thesis: M2 |= H
then M1 |= H by A2;
then M1 |= S by A4;
then M2 |= S by A1, A3;
hence M2 |= H by A4; :: thesis: verum

end;

assume A5: for H being ZF-formula st H in F holds
M2 |= H ; :: according to ZFREFLE1:def 1 :: thesis: M1 |= F
let H be ZF-formula; :: according to ZFREFLE1:def 1 :: thesis: ( H in F implies M1 |= H )
consider S being ZF-formula such that
A6: Free S = {} and
A7: for M being non empty set holds
( M |= S iff M |= H ) by Th6;
assume H in F ; :: thesis: M1 |= H
then M2 |= H by A5;
then M2 |= S by A7;
then M1 |= S by A1, A6;
hence M1 |= H by A7; :: thesis: verum

end;

assume A8: for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) ; :: thesis: M1 <==> M2
let H be ZF-formula; :: according to ZFREFLE1:def 2 :: thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) )
assume Free H = {} ; :: thesis: ( M1 |= H iff M2 |= H )
H in WFF by ZF_LANG:4;
then reconsider F = {H} as Subset of WFF by ZFMISC_1:31;
thus ( M1 |= H implies M2 |= H ) :: thesis: ( M2 |= H implies M1 |= H )

proof

assume M1 |= H ; :: thesis: M2 |= H
then for S being ZF-formula st S in F holds
M1 |= S by TARSKI:def 1;
then M1 |= F ;
then A9: M2 |= F by A8;
H in F by TARSKI:def 1;
hence M2 |= H by A9; :: thesis: verum

end;

assume M2 |= H ; :: thesis: M1 |= H
then for S being ZF-formula st S in F holds
M2 |= S by TARSKI:def 1;
then M2 |= F ;
then A10: M1 |= F by A8;
H in F by TARSKI:def 1;
hence M1 |= H by A10; :: thesis: verum