Theorem peano2 7929

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 7920	. 2 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
2	1	biimpi 216	1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2108  suc csuc 6397  ωcom 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-om 7904

This theorem is referenced by:  onnseq  8400  seqomlem1  8506  seqomlem4  8509  onasuc  8584  onmsuc  8585  onesuc  8586  o2p2e4  8597  nnacl  8667  nnecl  8669  nnacom  8673  nnmsucr  8681  nnaordex2  8695  1onnALT  8697  2onnALT  8699  3onn  8700  4onn  8701  nnneo  8711  nneob  8712  omopthlem1  8715  eldifsucnn  8720  findcard  9229  unfi  9238  phplem1  9270  php  9273  onomeneqOLD  9292  dif1ennnALT  9339  unbnn2  9361  dffi3  9500  wofib  9614  axinf2  9709  dfom3  9716  noinfep  9729  cantnflt  9741  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  trcl  9797  cardsucnn  10054  harsucnn  10067  dif1card  10079  fseqdom  10095  alephfp  10177  ackbij1lem5  10292  ackbij1lem16  10303  ackbij2lem2  10308  ackbij2lem3  10309  ackbij2  10311  sornom  10346  infpssrlem4  10375  fin23lem26  10394  fin23lem20  10406  fin23lem38  10418  fin23lem39  10419  isf32lem2  10423  isf32lem3  10424  isf34lem7  10448  isf34lem6  10449  fin1a2lem6  10474  fin1a2lem9  10477  fin1a2lem12  10480  domtriomlem  10511  axdc2lem  10517  axdc3lem  10519  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  axdclem2  10589  peano2nn  12305  om2uzrani  14003  uzrdgsuci  14011  fzennn  14019  axdc4uzlem  14034  precsexlem4  28252  precsexlem5  28253  precsexlem11  28259  noseqp1  28315  om2noseqlt  28323  noseqrdgsuc  28332  n0sbday  28372  dfnns2  28380  pw2bday  28436  zs12bday  28442  bnj970  34923  satfvsuc  35329  satfvsucsuc  35333  gonarlem  35362  goalrlem  35364  satffunlem2lem2  35374  satffunlem2  35376  ex-sategoelelomsuc  35394  elhf2  36139  0hf  36141  hfsn  36143  hfpw  36149  neibastop2lem  36326  exrecfnlem  37345  finxpsuclem  37363  domalom  37370  onexoegt  43205  nnoeomeqom  43274  nna1iscard  43507