Theorem bj-nfext

Description: Closed form of nfex . (Contributed by BJ, 10-Oct-2019)

	Ref	Expression
Assertion	bj-nfext	$$⊢\forall xℲy\phi \to Ⅎy\exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		nf5	$$⊢Ⅎy\phi \leftrightarrow \forall y\left(\phi \to \forall y\phi \right)$$
2	1	biimpi	$$⊢Ⅎy\phi \to \forall y\left(\phi \to \forall y\phi \right)$$
3	2	alimi	$$⊢\forall xℲy\phi \to \forall x\forall y\left(\phi \to \forall y\phi \right)$$
4		nfa2	$$⊢Ⅎy\forall x\forall y\left(\phi \to \forall y\phi \right)$$
5		bj-hbext	$$⊢\forall x\forall y\left(\phi \to \forall y\phi \right)\to \left(\exists x\phi \to \forall y\exists x\phi \right)$$
6	4 5	alrimi	$$⊢\forall x\forall y\left(\phi \to \forall y\phi \right)\to \forall y\left(\exists x\phi \to \forall y\exists x\phi \right)$$
7	3 6	syl	$$⊢\forall xℲy\phi \to \forall y\left(\exists x\phi \to \forall y\exists x\phi \right)$$
8		nf5	$$⊢Ⅎy\exists x\phi \leftrightarrow \forall y\left(\exists x\phi \to \forall y\exists x\phi \right)$$
9	7 8	sylibr	$$⊢\forall xℲy\phi \to Ⅎy\exists x\phi$$