theorem :: ZF_LANG1:187

for H being ZF-formula
for x, y being Variable holds variables_in (H / (x,y)) c= ((variables_in H) \ {x}) \/ {y}