Theorem peano2 7834

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

Proof of Theorem peano2

Step	Hyp	Ref	Expression
1		peano2b 7827	. 2 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
2	1	biimpi 216	1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2114  suc csuc 6319  ωcom 7810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-om 7811

This theorem is referenced by:  onnseq  8277  seqomlem1  8382  seqomlem4  8385  onasuc  8456  onmsuc  8457  onesuc  8458  o2p2e4  8469  nnacl  8540  nnecl  8542  nnacom  8546  nnmsucr  8554  nnaordex2  8568  1onnALT  8570  2onnALT  8572  3onn  8573  4onn  8574  nnneo  8584  nneob  8585  omopthlem1  8588  eldifsucnn  8593  findcard  9091  unfi  9098  phplem1  9131  php  9134  dif1ennnALT  9180  unbnn2  9200  dffi3  9337  wofib  9453  axinf2  9552  dfom3  9559  noinfep  9572  cantnflt  9584  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  trcl  9640  cardsucnn  9900  harsucnn  9913  dif1card  9923  fseqdom  9939  alephfp  10021  ackbij1lem5  10136  ackbij1lem16  10147  ackbij2lem2  10152  ackbij2lem3  10153  ackbij2  10155  sornom  10190  infpssrlem4  10219  fin23lem26  10238  fin23lem20  10250  fin23lem38  10262  fin23lem39  10263  isf32lem2  10267  isf32lem3  10268  isf34lem7  10292  isf34lem6  10293  fin1a2lem6  10318  fin1a2lem9  10321  fin1a2lem12  10324  domtriomlem  10355  axdc2lem  10361  axdc3lem  10363  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  axdclem2  10433  peano2nn  12177  om2uzrani  13905  uzrdgsuci  13913  fzennn  13921  axdc4uzlem  13936  precsexlem4  28216  precsexlem5  28217  precsexlem11  28223  noseqp1  28297  om2noseqlt  28305  noseqrdgsuc  28314  n0bday  28358  dfnns2  28378  z12bdaylem  28490  constrextdg2lem  33908  bnj970  35105  fineqvnttrclselem3  35283  noinfepfnregs  35292  noinfepregs  35293  satfvsuc  35559  satfvsucsuc  35563  gonarlem  35592  goalrlem  35594  satffunlem2lem2  35604  satffunlem2  35606  ex-sategoelelomsuc  35624  elhf2  36373  0hf  36375  hfsn  36377  hfpw  36383  neibastop2lem  36558  ttctr  36691  dfttc2g  36704  mh-inf3f1  36739  exrecfnlem  37709  finxpsuclem  37727  domalom  37734  onexoegt  43690  nnoeomeqom  43758  nna1iscard  43990  orbitcl  45402  omssaxinf2  45433