let M1, M2 be non empty set ; :: thesis: ( M1 <==> M2 iff for H being ZF-formula holds

( M1 |= H iff M2 |= H ) )

thus ( M1 <==> M2 implies for H being ZF-formula holds

( M1 |= H iff M2 |= H ) ) :: thesis: ( ( for H being ZF-formula holds

( M1 |= H iff M2 |= H ) ) implies M1 <==> M2 )

( M1 |= H iff M2 |= H ) ; :: thesis: M1 <==> M2

let H be ZF-formula; :: according to ZFREFLE1:def 2 :: thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) )

thus ( Free H = {} implies ( M1 |= H iff M2 |= H ) ) by A4; :: thesis: verum

( M1 |= H iff M2 |= H ) )

thus ( M1 <==> M2 implies for H being ZF-formula holds

( M1 |= H iff M2 |= H ) ) :: thesis: ( ( for H being ZF-formula holds

( M1 |= H iff M2 |= H ) ) implies M1 <==> M2 )

proof

assume A4:
for H being ZF-formula holds
assume A1:
for H being ZF-formula st Free H = {} holds

( M1 |= H iff M2 |= H ) ; :: according to ZFREFLE1:def 2 :: thesis: for H being ZF-formula holds

( M1 |= H iff M2 |= H )

let H be ZF-formula; :: thesis: ( M1 |= H iff M2 |= H )

consider S being ZF-formula such that

A2: Free S = {} and

A3: for M being non empty set holds

( M |= S iff M |= H ) by Th6;

( M1 |= S iff M2 |= S ) by A1, A2;

hence ( M1 |= H iff M2 |= H ) by A3; :: thesis: verum

end;( M1 |= H iff M2 |= H ) ; :: according to ZFREFLE1:def 2 :: thesis: for H being ZF-formula holds

( M1 |= H iff M2 |= H )

let H be ZF-formula; :: thesis: ( M1 |= H iff M2 |= H )

consider S being ZF-formula such that

A2: Free S = {} and

A3: for M being non empty set holds

( M |= S iff M |= H ) by Th6;

( M1 |= S iff M2 |= S ) by A1, A2;

hence ( M1 |= H iff M2 |= H ) by A3; :: thesis: verum

( M1 |= H iff M2 |= H ) ; :: thesis: M1 <==> M2

let H be ZF-formula; :: according to ZFREFLE1:def 2 :: thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) )

thus ( Free H = {} implies ( M1 |= H iff M2 |= H ) ) by A4; :: thesis: verum