Metamath Proof Explorer

Theorem nfnfc1

Description: The setvar x is bound in F/_ x A . (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Assertion nfnfc1 
|- F/ x F/_ x A

Proof

Step Hyp Ref Expression
1 df-nfc 
 |-  ( F/_ x A <-> A. y F/ x y e. A )
2 nfnf1 
 |-  F/ x F/ x y e. A
3 2 nfal 
 |-  F/ x A. y F/ x y e. A
4 1 3 nfxfr 
 |-  F/ x F/_ x A