Theorem peano2 7842

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

Syntax hints:   → wi 4   ∈ wcel 2114  suc csuc 6327  ωcom 7818

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-om 7819

This theorem is referenced by:  onnseq  8286  seqomlem1  8391  seqomlem4  8394  onasuc  8465  onmsuc  8466  onesuc  8467  o2p2e4  8478  nnacl  8549  nnecl  8551  nnacom  8555  nnmsucr  8563  nnaordex2  8577  1onnALT  8579  2onnALT  8581  3onn  8582  4onn  8583  nnneo  8593  nneob  8594  omopthlem1  8597  eldifsucnn  8602  findcard  9100  unfi  9107  phplem1  9140  php  9143  dif1ennnALT  9189  unbnn2  9209  dffi3  9346  wofib  9462  axinf2  9561  dfom3  9568  noinfep  9581  cantnflt  9593  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  trcl  9649  cardsucnn  9909  harsucnn  9922  dif1card  9932  fseqdom  9948  alephfp  10030  ackbij1lem5  10145  ackbij1lem16  10156  ackbij2lem2  10161  ackbij2lem3  10162  ackbij2  10164  sornom  10199  infpssrlem4  10228  fin23lem26  10247  fin23lem20  10259  fin23lem38  10271  fin23lem39  10272  isf32lem2  10276  isf32lem3  10277  isf34lem7  10301  isf34lem6  10302  fin1a2lem6  10327  fin1a2lem9  10330  fin1a2lem12  10333  domtriomlem  10364  axdc2lem  10370  axdc3lem  10372  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  axdclem2  10442  peano2nn  12169  om2uzrani  13887  uzrdgsuci  13895  fzennn  13903  axdc4uzlem  13918  precsexlem4  28218  precsexlem5  28219  precsexlem11  28225  noseqp1  28299  om2noseqlt  28307  noseqrdgsuc  28316  n0bday  28360  dfnns2  28380  z12bdaylem  28492  constrextdg2lem  33925  bnj970  35122  fineqvnttrclselem3  35298  noinfepfnregs  35307  noinfepregs  35308  satfvsuc  35574  satfvsucsuc  35578  gonarlem  35607  goalrlem  35609  satffunlem2lem2  35619  satffunlem2  35621  ex-sategoelelomsuc  35639  elhf2  36388  0hf  36390  hfsn  36392  hfpw  36398  neibastop2lem  36573  exrecfnlem  37631  finxpsuclem  37649  domalom  37656  onexoegt  43598  nnoeomeqom  43666  nna1iscard  43898  orbitcl  45310  omssaxinf2  45341