Theorem nfrab

Description: A variable not free in a wff remains so in a restricted class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfrabw when possible. (Contributed by NM, 13-Oct-2003) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfrab.1	$$⊢Ⅎx\phi$$
	nfrab.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfrab	$$⊢\underset{\_}{Ⅎ}x\left\{y\in A|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfrab.1	$$⊢Ⅎx\phi$$
2		nfrab.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-rab	$$⊢\left\{y\in A|\phi \right\}=\left\{y|\left(y\in A\wedge \phi \right)\right\}$$
4		nftru	$$⊢Ⅎy\top$$
5	2	nfcri	$$⊢Ⅎxz\in A$$
6		eleq1w	$$⊢z=y\to \left(z\in A\leftrightarrow y\in A\right)$$
7	5 6	dvelimnf	$$⊢\neg \forall xx=y\to Ⅎxy\in A$$
8	1	a1i	$$⊢\neg \forall xx=y\to Ⅎx\phi$$
9	7 8	nfand	$$⊢\neg \forall xx=y\to Ⅎx\left(y\in A\wedge \phi \right)$$
10	9	adantl	$$⊢\left(\top \wedge \neg \forall xx=y\right)\to Ⅎx\left(y\in A\wedge \phi \right)$$
11	4 10	nfabd2	$$⊢\top \to \underset{\_}{Ⅎ}x\left\{y|\left(y\in A\wedge \phi \right)\right\}$$
12	11	mptru	$$⊢\underset{\_}{Ⅎ}x\left\{y|\left(y\in A\wedge \phi \right)\right\}$$
13	3 12	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left\{y\in A|\phi \right\}$$