Metamath Proof Explorer

Theorem peano4

Description: Two natural numbers are equal iff their successors are equal, i.e. the successor function is one-to-one. One of Peano's five postulates for arithmetic. Proposition 7.30(4) of TakeutiZaring p. 43. (Contributed by NM, 3-Sep-2003)

Ref Expression
Assertion peano4 ⊢ A ∈ ω ∧ B ∈ ω → suc ⁡ A = suc ⁡ B ↔ A = B

Proof

Step Hyp Ref Expression
1 nnon ⊢ A ∈ ω → A ∈ On
2 nnon ⊢ B ∈ ω → B ∈ On
3 suc11 ⊢ A ∈ On ∧ B ∈ On → suc ⁡ A = suc ⁡ B ↔ A = B
4 1 2 3 syl2an ⊢ A ∈ ω ∧ B ∈ ω → suc ⁡ A = suc ⁡ B ↔ A = B