Theorem nfsuc

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

	Ref	Expression
Hypothesis	nfsuc.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfsuc	$$⊢\underset{\_}{Ⅎ}x\mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		nfsuc.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
3	1	nfsn	$$⊢\underset{\_}{Ⅎ}x\left\{A\right\}$$
4	1 3	nfun	$$⊢\underset{\_}{Ⅎ}x\left(A\cup \left\{A\right\}\right)$$
5	2 4	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\mathrm{suc}A$$