Metamath Proof Explorer


Theorem nn0suc

Description: A natural number is either 0 or a successor. (Contributed by NM, 27-May-1998)

Ref Expression
Assertion nn0suc AωA=xωA=sucx

Proof

Step Hyp Ref Expression
1 df-ne A¬A=
2 nnsuc AωAxωA=sucx
3 1 2 sylan2br Aω¬A=xωA=sucx
4 3 ex Aω¬A=xωA=sucx
5 4 orrd AωA=xωA=sucx