Metamath Proof Explorer


Theorem nfrab1

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

Ref Expression
Assertion nfrab1 _ x x A | φ

Proof

Step Hyp Ref Expression
1 df-rab x A | φ = x | x A φ
2 nfab1 _ x x | x A φ
3 1 2 nfcxfr _ x x A | φ