Theorem nfald2

Description: Variation on nfald 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 nfald 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	nfald2	$$⊢\phi \to Ⅎx\forall 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		nfnae	$$⊢Ⅎy\neg \forall xx=y$$
4	1 3	nfan	$$⊢Ⅎy\left(\phi \wedge \neg \forall xx=y\right)$$
5	4 2	nfald	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\forall y\psi$$
6	5	ex	$$⊢\phi \to \left(\neg \forall xx=y\to Ⅎx\forall y\psi \right)$$
7		nfa1	$$⊢Ⅎy\forall y\psi$$
8		biidd	$$⊢\forall xx=y\to \left(\forall y\psi \leftrightarrow \forall y\psi \right)$$
9	8	drnf1	$$⊢\forall xx=y\to \left(Ⅎx\forall y\psi \leftrightarrow Ⅎy\forall y\psi \right)$$
10	7 9	mpbiri	$$⊢\forall xx=y\to Ⅎx\forall y\psi$$
11	6 10	pm2.61d2	$$⊢\phi \to Ⅎx\forall y\psi$$