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 = {} & ( 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 A3;
then M2 |= S by A1, A3;
hence M2 |= H by A3; :: thesis: verum

end;

assume A4: 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
A5: ( Free S = {} & ( 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 A4;
then M2 |= S by A5;
then M1 |= S by A1, A5;
hence M1 |= H by A5; :: thesis: verum

end;

assume A6: 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:14;
then reconsider F = {H} as Subset of WFF by ZFMISC_1:37;
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 by Def1;
then ( M2 |= F & H in F ) by A6, TARSKI:def 1;
hence M2 |= H by Def1; :: 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 by Def1;
then ( M1 |= F & H in F ) by A6, TARSKI:def 1;
hence M1 |= H by Def1; :: thesis: verum