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

set v = the Function of VAR,M;
set m = the 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 = the Element of M as set ;
take a ; :: thesis: {a} = M
thus {a} c= M by ZFMISC_1:31; :: according to XBOOLE_0:def 10 :: thesis: M c= {a}
let b be object ; :: 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,( the Function of VAR,M / (x, the Element of M)) / (y,b) |= x '=' y by A1;
then A5: (( the Function of VAR,M / (x, the Element of M)) / (y,b)) . x = (( the Function of VAR,M / (x, the Element of M)) / (y,b)) . y by ZF_MODEL:12;
A6: ( ( the Function of VAR,M / (x, the Element of M)) . x = the Element of M & (( the Function of VAR,M / (x, the Element of M)) / (y,b)) . y = b ) by FUNCT_7:128;
(( the Function of VAR,M / (x, the Element of M)) / (y,b)) . x = ( the Function of VAR,M / (x, the Element of M)) . x by A2, FUNCT_7:32;
hence contradiction by A4, A5, A6, TARSKI:def 1; :: thesis: verum

end;

now :: thesis: ( ex a being set st {a} = M implies for v being Function of VAR,M holds M,v |= x '=' y )

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 Th79; :: thesis: verum