Theorem nfexd

Description: If x is not free in ps , then it is not free in E. y ps . (Contributed by Mario Carneiro, 24-Sep-2016)

	Ref	Expression
Hypotheses	nfald.1	$$⊢Ⅎy\phi$$
	nfald.2	$$⊢\phi \to Ⅎx\psi$$
Assertion	nfexd	$$⊢\phi \to Ⅎx\exists y\psi$$

Proof

Step	Hyp	Ref	Expression
1		nfald.1	$$⊢Ⅎy\phi$$
2		nfald.2	$$⊢\phi \to Ⅎx\psi$$
3		df-ex	$$⊢\exists y\psi \leftrightarrow \neg \forall y\neg \psi$$
4	2	nfnd	$$⊢\phi \to Ⅎx\neg \psi$$
5	1 4	nfald	$$⊢\phi \to Ⅎx\forall y\neg \psi$$
6	5	nfnd	$$⊢\phi \to Ⅎx\neg \forall y\neg \psi$$
7	3 6	nfxfrd	$$⊢\phi \to Ⅎx\exists y\psi$$