let H be ZF-formula; for x, y, z being Variable holds variables_in (Ex (x,y,z,H)) = (variables_in H) \/ {x,y,z}
let x, y, z be Variable; variables_in (Ex (x,y,z,H)) = (variables_in H) \/ {x,y,z}
thus variables_in (Ex (x,y,z,H)) =
(variables_in (Ex (y,z,H))) \/ {x}
by Th146
.=
((variables_in H) \/ {y,z}) \/ {x}
by Th148
.=
(variables_in H) \/ ({y,z} \/ {x})
by XBOOLE_1:4
.=
(variables_in H) \/ {y,z,x}
by ENUMSET1:3
.=
(variables_in H) \/ {x,y,z}
by ENUMSET1:59
; verum