theorem :: ZF_LANG1:87

for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is conjunctive holds
( M,v |= H iff ( M,v |= the_left_argument_of H & M,v |= the_right_argument_of H ) )