Theorem nnon 7812

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

Syntax hints:   → wi 4   ∈ wcel 2109  Oncon0 6311  ω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

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 3397  df-ss 3922  df-om 7807

This theorem is referenced by:  nnoni  7813  nnord  7814  peano4  7832  findsg  7837  onasuc  8453  onmsuc  8454  nna0  8529  nnm0  8530  nnasuc  8531  nnmsuc  8532  nnesuc  8533  nnecl  8538  nnawordi  8546  nnmword  8558  nnawordex  8562  nnaordex  8563  oaabslem  8572  oaabs  8573  oaabs2  8574  omabslem  8575  omabs  8576  nnneo  8580  nneob  8581  naddoa  8627  omnaddcl  8628  dif1ennn  9085  findcard2  9088  onfin2  9140  nndomo  9141  findcard3  9187  findcard3OLD  9188  dffi3  9340  card2inf  9466  elom3  9563  cantnfp1lem3  9595  cnfcomlem  9614  cnfcom  9615  cnfcom3  9619  ttrcltr  9631  ttrclselem1  9640  ttrclselem2  9641  finnum  9863  cardnn  9878  nnsdomel  9905  harsucnn  9913  nnadjuALT  10112  ficardun2  10115  ackbij1lem15  10146  ackbij2lem2  10152  ackbij2lem3  10153  ackbij2  10155  fin23lem22  10240  isf32lem5  10270  fin1a2lem4  10316  fin1a2lem9  10321  pwfseqlem3  10573  winainflem  10606  wunr1om  10632  tskr1om  10680  grothomex  10742  pion  10792  om2uzlt2i  13877  madefi  27846  oldfi  27847  precsexlem3  28135  precsexlem4  28136  precsexlem5  28137  om2noseqlt  28217  om2noseqlt2  28218  zs12bday  28380  constrfin  33732  constrextdg2lem  33734  constrext2chnlem  33736  constrfiss  33737  constrllcllem  33738  constrlccllem  33739  constrcccllem  33740  constrcn  33746  constrcjcl  33754  bnj168  34716  satfvsuc  35353  satf0suc  35368  sat1el2xp  35371  fmlasuc0  35376  elhf2  36168  findreccl  36446  rdgeqoa  37363  exrecfnlem  37372  finxpreclem4  37387  finxpreclem6  37389  harinf  43027  onexoegt  43237  oaabsb  43287  nnoeomeqom  43305  cantnfub  43314  dflim5  43322  onmcl  43324  omabs2  43325  tfsconcat0b  43339  naddcnffo  43357  naddonnn  43388  naddwordnexlem0  43389  naddwordnexlem3  43392  oawordex3  43393  naddwordnexlem4  43394  omssrncard  43533  nna1iscard  43538