Theorem nfsuc

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

	Ref	Expression
Hypothesis	nfsuc.1	⊢ Ⅎ 𝑥 𝐴
Assertion	nfsuc	⊢ Ⅎ 𝑥 suc 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfsuc.1	⊢ Ⅎ 𝑥 𝐴
2		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
3	1	nfsn	⊢ Ⅎ 𝑥 { 𝐴 }
4	1 3	nfun	⊢ Ⅎ 𝑥 ( 𝐴 ∪ { 𝐴 } )
5	2 4	nfcxfr	⊢ Ⅎ 𝑥 suc 𝐴