theorem :: ZFREFLE1:7

for M1, M2 being non empty set holds
( M1 <==> M2 iff for H being ZF-formula holds
( M1 |= H iff M2 |= H ) )