Theorem nnon 7828

Description: A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)

Assertion

Ref	Expression
nnon	⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Proof of Theorem nnon

Step	Hyp	Ref	Expression
1		omsson 7826	. 2 ⊢ ω ⊆ On
2	1	sseli 3939	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2109  Oncon0 6320  ωcom 7822

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-ss 3928  df-om 7823

This theorem is referenced by:  nnoni  7829  nnord  7830  peano4  7848  findsg  7853  onasuc  8469  onmsuc  8470  nna0  8545  nnm0  8546  nnasuc  8547  nnmsuc  8548  nnesuc  8549  nnecl  8554  nnawordi  8562  nnmword  8574  nnawordex  8578  nnaordex  8579  oaabslem  8588  oaabs  8589  oaabs2  8590  omabslem  8591  omabs  8592  nnneo  8596  nneob  8597  naddoa  8643  omnaddcl  8644  dif1ennn  9102  findcard2  9105  onfin2  9157  nndomo  9158  findcard3  9205  findcard3OLD  9206  dffi3  9358  card2inf  9484  elom3  9577  cantnfp1lem3  9609  cnfcomlem  9628  cnfcom  9629  cnfcom3  9633  ttrcltr  9645  ttrclselem1  9654  ttrclselem2  9655  finnum  9877  cardnn  9892  nnsdomel  9919  harsucnn  9927  nnadjuALT  10128  ficardun2  10131  ackbij1lem15  10162  ackbij2lem2  10168  ackbij2lem3  10169  ackbij2  10171  fin23lem22  10256  isf32lem5  10286  fin1a2lem4  10332  fin1a2lem9  10337  pwfseqlem3  10589  winainflem  10622  wunr1om  10648  tskr1om  10696  grothomex  10758  pion  10808  om2uzlt2i  13892  madefi  27800  oldfi  27801  precsexlem3  28087  precsexlem4  28088  precsexlem5  28089  om2noseqlt  28169  om2noseqlt2  28170  zs12bday  28319  constrfin  33709  constrextdg2lem  33711  constrext2chnlem  33713  constrfiss  33714  constrllcllem  33715  constrlccllem  33716  constrcccllem  33717  constrcn  33723  constrcjcl  33731  bnj168  34693  satfvsuc  35321  satf0suc  35336  sat1el2xp  35339  fmlasuc0  35344  elhf2  36136  findreccl  36414  rdgeqoa  37331  exrecfnlem  37340  finxpreclem4  37355  finxpreclem6  37357  harinf  42996  onexoegt  43206  oaabsb  43256  nnoeomeqom  43274  cantnfub  43283  dflim5  43291  onmcl  43293  omabs2  43294  tfsconcat0b  43308  naddcnffo  43326  naddonnn  43357  naddwordnexlem0  43358  naddwordnexlem3  43361  oawordex3  43362  naddwordnexlem4  43363  omssrncard  43502  nna1iscard  43507