theorem :: ZF_MODEL:13

for E being non empty set
for f being Function of VAR,E
for x, y being Variable holds
( E,f |= x 'in' y iff f . x in f . y ) by Th3;