theorem :: ZF_LANG1:82

for x, y being Variable
for M being non empty set holds
( M |= x '=' y iff ( x = y or ex a being set st {a} = M ) )