Theorem nnon 7837

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 7835	. 2 ⊢ ω ⊆ On
2	1	sseli 3923	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2132  Oncon0 6331  ωcom 7831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-ss 3912  df-om 7832

This theorem is referenced by:  nnoni  7838  nnord  7839  peano4  7858  findsg  7863  onasuc  8481  onmsuc  8482  nna0  8558  nnm0  8559  nnasuc  8560  nnmsuc  8561  nnesuc  8562  nnecl  8567  nnawordi  8575  nnmword  8587  nnawordex  8591  nnaordex  8592  oaabslem  8601  oaabs  8602  oaabs2  8603  omabslem  8604  omabs  8605  nnneo  8609  nneob  8610  naddoa  8657  omnaddcl  8658  dif1ennn  9116  findcard2  9118  onfin2  9170  nndomo  9171  findcard3  9212  dffi3  9363  card2inf  9489  elom3  9589  cantnfp1lem3  9621  cnfcomlem  9640  cnfcom  9641  cnfcom3  9645  ttrcltr  9657  ttrclselem1  9666  ttrclselem2  9667  finnum  9892  cardnn  9907  nnsdomel  9934  harsucnn  9942  nnadjuALT  10141  ficardun2  10144  ackbij1lem15  10175  ackbij2lem2  10181  ackbij2lem3  10182  ackbij2  10184  fin23lem22  10270  isf32lem5  10300  fin1a2lem4  10346  fin1a2lem9  10351  pwfseqlem3  10604  winainflem  10637  wunr1om  10663  tskr1om  10711  grothomex  10773  pion  10823  om2uzlt2i  13950  madefi  27972  oldfi  27973  precsexlem3  28268  precsexlem4  28269  precsexlem5  28270  om2noseqlt  28358  om2noseqlt2  28359  constrfin  33987  constrextdg2lem  33989  constrext2chnlem  33991  constrfiss  33992  constrllcllem  33993  constrlccllem  33994  constrcccllem  33995  constrcn  34001  constrcjcl  34009  bnj168  34973  fineqvnttrclselem1  35362  fineqvnttrclselem2  35363  fineqvnttrclse  35365  satfvsuc  35649  satf0suc  35664  sat1el2xp  35667  fmlasuc0  35672  elhf2  36463  findreccl  36751  ttctr  36791  ttcmin  36794  dfttc2g  36804  rdgeqoa  37802  exrecfnlem  37811  finxpreclem4  37826  finxpreclem6  37828  harinf  43549  onexoegt  43759  oaabsb  43809  nnoeomeqom  43827  cantnfub  43836  dflim5  43844  onmcl  43846  omabs2  43847  tfsconcat0b  43861  naddcnffo  43879  naddonnn  43910  naddwordnexlem0  43911  naddwordnexlem3  43914  oawordex3  43915  naddwordnexlem4  43916  omssrncard  44054  nna1iscard  44059