Theorem nfrab1

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

	Ref	Expression
Assertion	nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
3	1 2	nfcxfr	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝜑 }