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 e. _om /\ B e. _om ) -> ( suc A = suc B <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( A e. _om -> A e. On )
2		nnon	|- ( B e. _om -> B e. On )
3		suc11	|- ( ( A e. On /\ B e. On ) -> ( suc A = suc B <-> A = B ) )
4	1 2 3	syl2an	|- ( ( A e. _om /\ B e. _om ) -> ( suc A = suc B <-> A = B ) )