theorem :: ZF_LANG1:185

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