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	$$⊢Ⅎx\phi$$
Assertion	nfex	$$⊢Ⅎx\exists y\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfex.1	$$⊢Ⅎx\phi$$
2		df-ex	$$⊢\exists y\phi \leftrightarrow \neg \forall y\neg \phi$$
3	1	nfn	$$⊢Ⅎx\neg \phi$$
4	3	nfal	$$⊢Ⅎx\forall y\neg \phi$$
5	4	nfn	$$⊢Ⅎx\neg \forall y\neg \phi$$
6	2 5	nfxfr	$$⊢Ⅎx\exists y\phi$$