Theorem peano2 7886

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

Syntax hints:   → wi 4   ∈ wcel 2108  suc csuc 6354  ωcom 7861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-om 7862

This theorem is referenced by:  onnseq  8358  seqomlem1  8464  seqomlem4  8467  onasuc  8540  onmsuc  8541  onesuc  8542  o2p2e4  8553  nnacl  8623  nnecl  8625  nnacom  8629  nnmsucr  8637  nnaordex2  8651  1onnALT  8653  2onnALT  8655  3onn  8656  4onn  8657  nnneo  8667  nneob  8668  omopthlem1  8671  eldifsucnn  8676  findcard  9177  unfi  9185  phplem1  9218  php  9221  onomeneqOLD  9238  dif1ennnALT  9283  unbnn2  9305  dffi3  9443  wofib  9559  axinf2  9654  dfom3  9661  noinfep  9674  cantnflt  9686  ttrcltr  9730  ttrclss  9734  ttrclselem2  9740  trcl  9742  cardsucnn  9999  harsucnn  10012  dif1card  10024  fseqdom  10040  alephfp  10122  ackbij1lem5  10237  ackbij1lem16  10248  ackbij2lem2  10253  ackbij2lem3  10254  ackbij2  10256  sornom  10291  infpssrlem4  10320  fin23lem26  10339  fin23lem20  10351  fin23lem38  10363  fin23lem39  10364  isf32lem2  10368  isf32lem3  10369  isf34lem7  10393  isf34lem6  10394  fin1a2lem6  10419  fin1a2lem9  10422  fin1a2lem12  10425  domtriomlem  10456  axdc2lem  10462  axdc3lem  10464  axdc3lem2  10465  axdc3lem4  10467  axdc4lem  10469  axdclem2  10534  peano2nn  12252  om2uzrani  13970  uzrdgsuci  13978  fzennn  13986  axdc4uzlem  14001  precsexlem4  28164  precsexlem5  28165  precsexlem11  28171  noseqp1  28237  om2noseqlt  28245  noseqrdgsuc  28254  n0sbday  28296  dfnns2  28313  zs12bday  28395  constrextdg2lem  33782  bnj970  34978  satfvsuc  35383  satfvsucsuc  35387  gonarlem  35416  goalrlem  35418  satffunlem2lem2  35428  satffunlem2  35430  ex-sategoelelomsuc  35448  elhf2  36193  0hf  36195  hfsn  36197  hfpw  36203  neibastop2lem  36378  exrecfnlem  37397  finxpsuclem  37415  domalom  37422  onexoegt  43268  nnoeomeqom  43336  nna1iscard  43569  orbitcl  44982  omssaxinf2  45013