theorem Th184: :: ZF_LANG1:184

for H being ZF-formula
for x, y being Variable st x <> y holds
not x in variables_in (H / (x,y))