:: deftheorem defines is_elementary_subsystem_of ZFREFLE1:def 3 :
for M1, M2 being non empty set holds
( M1 is_elementary_subsystem_of M2 iff ( M1 c= M2 & ( for H being ZF-formula
for v being Function of VAR,M1 holds
( M1,v |= H iff M2,M2 ! v |= H ) ) ) );