Theorem hbex

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

	Ref	Expression
Hypothesis	hbex.1	$$⊢\phi \to \forall x\phi$$
Assertion	hbex	$$⊢\exists y\phi \to \forall x\exists y\phi$$

Proof

Step	Hyp	Ref	Expression
1		hbex.1	$$⊢\phi \to \forall x\phi$$
2	1	nf5i	$$⊢Ⅎx\phi$$
3	2	nfex	$$⊢Ⅎx\exists y\phi$$
4	3	nf5ri	$$⊢\exists y\phi \to \forall x\exists y\phi$$