This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfsuc

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

Ref Expression
Hypothesis nfsuc.1 ⊢ Ⅎ _ x A
Assertion nfsuc ⊢ Ⅎ _ x suc ⁡ A

Proof

Step Hyp Ref Expression
1 nfsuc.1 ⊢ Ⅎ _ x A
2 df-suc ⊢ suc ⁡ A = A ∪ A
3 1 nfsn ⊢ Ⅎ _ x A
4 1 3 nfun ⊢ Ⅎ _ x A ∪ A
5 2 4 nfcxfr ⊢ Ⅎ _ x suc ⁡ A