Theorem bj-nfexd

Description: Variant of nfexd . (Contributed by BJ, 25-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		bj-nfald.1	$$⊢\phi \to \forall y\phi$$
2		bj-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	bj-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$$