Theorem nfex

Description: If x is not free in ph , then it is not free in E. y ph . (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 30-Dec-2017) Reduce symbol count in nfex , hbex . (Revised by Wolf Lammen, 16-Oct-2021)

	Ref	Expression
Hypothesis	nfex.1	⊢ Ⅎ 𝑥 𝜑
Assertion	nfex	⊢ Ⅎ 𝑥 ∃ 𝑦 𝜑

Proof

Step	Hyp	Ref	Expression
1		nfex.1	⊢ Ⅎ 𝑥 𝜑
2		df-ex	⊢ ( ∃ 𝑦 𝜑 ↔ ¬ ∀ 𝑦 ¬ 𝜑 )
3	1	nfn	⊢ Ⅎ 𝑥 ¬ 𝜑
4	3	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 ¬ 𝜑
5	4	nfn	⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑
6	2 5	nfxfr	⊢ Ⅎ 𝑥 ∃ 𝑦 𝜑