Theorem nfrab1

Description: The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997)

	Ref	Expression
Assertion	nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
2		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
3	1 2	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|\phi \right\}$$