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 
|- F/_ x { x e. A | ph }

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
2 nfab1 
 |-  F/_ x { x | ( x e. A /\ ph ) }
3 1 2 nfcxfr 
 |-  F/_ x { x e. A | ph }