Theorem nfexd2

Description: Variation on nfexd which adds the hypothesis that x and y are distinct in the inner subproof. Usage of this theorem is discouraged because it depends on ax-13 . Check out nfexd for a version requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfald2.1	$$⊢Ⅎy\phi$$
	nfald2.2	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\psi$$
Assertion	nfexd2	$$⊢\phi \to Ⅎx\exists y\psi$$

Proof

Step	Hyp	Ref	Expression
1		nfald2.1	$$⊢Ⅎy\phi$$
2		nfald2.2	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\psi$$
3		df-ex	$$⊢\exists y\psi \leftrightarrow \neg \forall y\neg \psi$$
4	2	nfnd	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\neg \psi$$
5	1 4	nfald2	$$⊢\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$$