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	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
2		nnon	⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
3		suc11	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵 ) )