Theorem peano2 6725

Description: The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)

Assertion

Ref	Expression
peano2	|- ( A e. om -> suc A e. om )

Proof of Theorem peano2

Step	Hyp	Ref	Expression
1		peano2b 6720	. 2 |- ( A e. om <-> suc A e. om )
2	1	biimpi 198	1 |- ( A e. om -> suc A e. om )

Syntax hints:   -> wi 4   e. wcel 1869   suc csuc 5442   omcom 6704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658  ax-un 6595

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-tr 4517  df-eprel 4762  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-om 6705

This theorem is referenced by:  onnseq  7069  seqomlem1  7173  seqomlem4  7176  onasuc  7236  onmsuc  7237  onesuc  7238  nnacl  7318  nnecl  7320  nnacom  7324  nnmsucr  7332  1onn  7346  2onn  7347  3onn  7348  4onn  7349  nnneo  7358  nneob  7359  omopthlem1  7362  onomeneq  7766  dif1en  7808  findcard  7814  findcard2  7815  unbnn2  7832  dffi3  7949  wofib  8064  axinf2  8149  dfom3  8156  noinfep  8168  cantnflt  8180  trcl  8215  cardsucnn  8422  dif1card  8444  fseqdom  8459  alephfp  8541  ackbij1lem16  8667  ackbij2lem2  8672  ackbij2lem3  8673  ackbij2  8675  sornom  8709  infpssrlem4  8738  fin23lem26  8757  fin23lem20  8769  fin23lem38  8781  fin23lem39  8782  isf32lem2  8786  isf32lem3  8787  isf34lem7  8811  isf34lem6  8812  fin1a2lem6  8837  fin1a2lem9  8840  fin1a2lem12  8843  domtriomlem  8874  axdc2lem  8880  axdc3lem  8882  axdc3lem2  8883  axdc3lem4  8885  axdc4lem  8887  axdclem2  8952  peano2nn  10623  om2uzrani  12167  uzrdgsuci  12175  fzennn  12182  axdc4uzlem  12196  bnj970  29760  trpredtr  30472  elhf2  30941  0hf  30943  hfsn  30945  hfpw  30951  neibastop2lem  31015  finxpsuclem  31747