Theorem peano2 7830

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

Syntax hints:   → wi 4   ∈ wcel 2109  suc csuc 6313  ωcom 7806

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-om 7807

This theorem is referenced by:  onnseq  8274  seqomlem1  8379  seqomlem4  8382  onasuc  8453  onmsuc  8454  onesuc  8455  o2p2e4  8466  nnacl  8536  nnecl  8538  nnacom  8542  nnmsucr  8550  nnaordex2  8564  1onnALT  8566  2onnALT  8568  3onn  8569  4onn  8570  nnneo  8580  nneob  8581  omopthlem1  8584  eldifsucnn  8589  findcard  9087  unfi  9095  phplem1  9128  php  9131  dif1ennnALT  9180  unbnn2  9202  dffi3  9340  wofib  9456  axinf2  9555  dfom3  9562  noinfep  9575  cantnflt  9587  ttrcltr  9631  ttrclss  9635  ttrclselem2  9641  trcl  9643  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  12158  om2uzrani  13877  uzrdgsuci  13885  fzennn  13893  axdc4uzlem  13908  precsexlem4  28135  precsexlem5  28136  precsexlem11  28142  noseqp1  28208  om2noseqlt  28216  noseqrdgsuc  28225  n0sbday  28267  dfnns2  28284  zs12bday  28379  constrextdg2lem  33717  bnj970  34916  satfvsuc  35336  satfvsucsuc  35340  gonarlem  35369  goalrlem  35371  satffunlem2lem2  35381  satffunlem2  35383  ex-sategoelelomsuc  35401  elhf2  36151  0hf  36153  hfsn  36155  hfpw  36161  neibastop2lem  36336  exrecfnlem  37355  finxpsuclem  37373  domalom  37380  onexoegt  43220  nnoeomeqom  43288  nna1iscard  43521  orbitcl  44934  omssaxinf2  44965