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

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