Metamath Proof Explorer

Theorem nfsuc

Description: Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003)

Ref Expression
Hypothesis nfsuc.1 
|- F/_ x A
Assertion nfsuc 
|- F/_ x suc A

Proof

Step Hyp Ref Expression
1 nfsuc.1 
 |-  F/_ x A
2 df-suc 
 |-  suc A = ( A u. { A } )
3 1 nfsn 
 |-  F/_ x { A }
4 1 3 nfun 
 |-  F/_ x ( A u. { A } )
5 2 4 nfcxfr 
 |-  F/_ x suc A