Theorem hbex

If \( x \) is not free in \( \varphi \), then it is not free in \( \exists y \, \varphi \). (Contributed by NM, 12-Mar-1993.) Reduce symbol count in nfex, hbex. (Revised by Wolf Lammen, 16-Oct-2021.)

Hypothesis
hbex.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
Conclusion
\( \vdash \exists y \, \varphi \rightarrow \forall x \, \exists y \, \varphi \)
Proof
hbex.1
nf5i _
nfex _
nf5ri _