theorem Th146: :: ZF_LANG1:146

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