let x, y be Variable; :: thesis: for M being non empty set holds
( M |= x '=' y iff ( x = y or ex a being set st {a} = M ) )
let M be non empty set ; :: thesis: ( M |= x '=' y iff ( x = y or ex a being set st {a} = M ) )
thus ( not M |= x '=' y or x = y or ex a being set st {a} = M ) :: thesis: ( ( x = y or ex a being set st {a} = M ) implies M |= x '=' y )

proof

consider v being Function of VAR ,M;
consider m being Element of M;
assume that
A1: for v being Function of VAR ,M holds M,v |= x '=' y and
A2: x <> y ; :: according to ZF_MODEL:def 5 :: thesis: ex a being set st {a} = M
reconsider a = m as set ;
take a ; :: thesis: {a} = M
thus {a} c= M by ZFMISC_1:37; :: according to XBOOLE_0:def 10 :: thesis: M c= {a}
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in M or b in {a} )
assume that
A3: b in M and
A4: not b in {a} ; :: thesis: contradiction
reconsider b = b as Element of M by A3;
M,(v / x,m) / y,b |= x '=' y by A1;
then A5: ((v / x,m) / y,b) . x = ((v / x,m) / y,b) . y by ZF_MODEL:12;
A6: ( (v / x,m) . x = m & ((v / x,m) / y,b) . y = b ) by FUNCT_7:130;
((v / x,m) / y,b) . x = (v / x,m) . x by A2, FUNCT_7:34;
hence contradiction by A4, A5, A6, TARSKI:def 1; :: thesis: verum

end;

now

given a being set such that A7: {a} = M ; :: thesis: for v being Function of VAR ,M holds M,v |= x '=' y
let v be Function of VAR ,M; :: thesis: M,v |= x '=' y
( v . x = a & v . y = a ) by A7, TARSKI:def 1;
hence M,v |= x '=' y by ZF_MODEL:12; :: thesis: verum

end;

hence ( ( x = y or ex a being set st {a} = M ) implies M |= x '=' y ) by Th90, ZF_MODEL:def 5; :: thesis: verum