Theorem nnon 7811

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

Syntax hints:   → wi 4   ∈ wcel 2113  Oncon0 6314  ωcom 7805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-ss 3915  df-om 7806

This theorem is referenced by:  nnoni  7812  nnord  7813  peano4  7831  findsg  7836  onasuc  8452  onmsuc  8453  nna0  8528  nnm0  8529  nnasuc  8530  nnmsuc  8531  nnesuc  8532  nnecl  8537  nnawordi  8545  nnmword  8557  nnawordex  8561  nnaordex  8562  oaabslem  8571  oaabs  8572  oaabs2  8573  omabslem  8574  omabs  8575  nnneo  8579  nneob  8580  naddoa  8626  omnaddcl  8627  dif1ennn  9083  findcard2  9085  onfin2  9136  nndomo  9137  findcard3  9178  dffi3  9326  card2inf  9452  elom3  9549  cantnfp1lem3  9581  cnfcomlem  9600  cnfcom  9601  cnfcom3  9605  ttrcltr  9617  ttrclselem1  9626  ttrclselem2  9627  finnum  9852  cardnn  9867  nnsdomel  9894  harsucnn  9902  nnadjuALT  10101  ficardun2  10104  ackbij1lem15  10135  ackbij2lem2  10141  ackbij2lem3  10142  ackbij2  10144  fin23lem22  10229  isf32lem5  10259  fin1a2lem4  10305  fin1a2lem9  10310  pwfseqlem3  10562  winainflem  10595  wunr1om  10621  tskr1om  10669  grothomex  10731  pion  10781  om2uzlt2i  13865  madefi  27878  oldfi  27879  precsexlem3  28167  precsexlem4  28168  precsexlem5  28169  om2noseqlt  28249  om2noseqlt2  28250  zs12bday  28414  constrfin  33831  constrextdg2lem  33833  constrext2chnlem  33835  constrfiss  33836  constrllcllem  33837  constrlccllem  33838  constrcccllem  33839  constrcn  33845  constrcjcl  33853  bnj168  34814  fineqvnttrclselem1  35213  fineqvnttrclselem2  35214  fineqvnttrclse  35216  satfvsuc  35477  satf0suc  35492  sat1el2xp  35495  fmlasuc0  35500  elhf2  36291  findreccl  36569  rdgeqoa  37487  exrecfnlem  37496  finxpreclem4  37511  finxpreclem6  37513  harinf  43191  onexoegt  43401  oaabsb  43451  nnoeomeqom  43469  cantnfub  43478  dflim5  43486  onmcl  43488  omabs2  43489  tfsconcat0b  43503  naddcnffo  43521  naddonnn  43552  naddwordnexlem0  43553  naddwordnexlem3  43556  oawordex3  43557  naddwordnexlem4  43558  omssrncard  43697  nna1iscard  43702