theorem :: ZF_LANG1:70

for p being ZF-formula
for x, y, z being Variable holds Free (Ex (x,y,z,p)) = (Free p) \ {x,y,z}