theorem :: ZF_LANG1:150

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