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