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 Gino Giotto, 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		nftru	$$⊢Ⅎy\top$$
5	2	nfcri	$$⊢Ⅎxy\in A$$
6	5 1	nfan	$$⊢Ⅎx\left(y\in A\wedge \phi \right)$$
7	6	a1i	$$⊢\top \to Ⅎx\left(y\in A\wedge \phi \right)$$
8	4 7	nfabdw	$$⊢\top \to \underset{\_}{Ⅎ}x\left\{y|\left(y\in A\wedge \phi \right)\right\}$$
9	8	mptru	$$⊢\underset{\_}{Ⅎ}x\left\{y|\left(y\in A\wedge \phi \right)\right\}$$
10	3 9	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left\{y\in A|\phi \right\}$$