theorem :: ZF_LANG1:91

for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is biconditional holds
( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) )