Theorem nfrabw

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 13-Oct-2003) Avoid ax-13 . (Revised by GG, 10-Jan-2024) (Proof shortened by Wolf Lammen, 23-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		nfrabw.1	$$⊢Ⅎx\phi$$
2		nfrabw.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-rab	$$⊢\left\{y\in A|\phi \right\}=\left\{y|\left(y\in A\wedge \phi \right)\right\}$$
4	2	nfcri	$$⊢Ⅎxy\in A$$
5	4 1	nfan	$$⊢Ⅎx\left(y\in A\wedge \phi \right)$$
6	5	nfab	$$⊢\underset{\_}{Ⅎ}x\left\{y|\left(y\in A\wedge \phi \right)\right\}$$
7	3 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left\{y\in A|\phi \right\}$$