Theorem nfabd2

Description: Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (Proof shortened by Wolf Lammen, 10-May-2023) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfabd2.1	$$⊢Ⅎy\phi$$
	nfabd2.2	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\psi$$
Assertion	nfabd2	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{y|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfabd2.1	$$⊢Ⅎy\phi$$
2		nfabd2.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	nfabd	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \underset{\_}{Ⅎ}x\left\{y|\psi \right\}$$
6	5	ex	$$⊢\phi \to \left(\neg \forall xx=y\to \underset{\_}{Ⅎ}x\left\{y|\psi \right\}\right)$$
7		nfab1	$$⊢\underset{\_}{Ⅎ}y\left\{y|\psi \right\}$$
8		eqidd	$$⊢\forall xx=y\to \left\{y|\psi \right\}=\left\{y|\psi \right\}$$
9	8	drnfc1	$$⊢\forall xx=y\to \left(\underset{\_}{Ⅎ}x\left\{y|\psi \right\}\leftrightarrow \underset{\_}{Ⅎ}y\left\{y|\psi \right\}\right)$$
10	7 9	mpbiri	$$⊢\forall xx=y\to \underset{\_}{Ⅎ}x\left\{y|\psi \right\}$$
11	6 10	pm2.61d2	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{y|\psi \right\}$$