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	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
Assertion	hbex	⊢ ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		hbex.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2	1	nf5i	⊢ Ⅎ 𝑥 𝜑
3	2	nfex	⊢ Ⅎ 𝑥 ∃ 𝑦 𝜑
4	3	nf5ri	⊢ ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 )