theorem Th66: :: ZF_LANG1:66

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