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 )

( 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 )

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

( 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 A8:
for F being Subset of WFF holds
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 )

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;( 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 A5:
for H being ZF-formula st H in F holds
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;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

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

( 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
M2 |= H
; :: thesis: M1 |= H
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;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

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