Theorem nnon 7894

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

Syntax hints:   → wi 4   ∈ wcel 2107  Oncon0 6383  ωcom 7888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-ss 3967  df-om 7889

This theorem is referenced by:  nnoni  7895  nnord  7896  peano4  7915  findsg  7920  onasuc  8567  onmsuc  8568  nna0  8643  nnm0  8644  nnasuc  8645  nnmsuc  8646  nnesuc  8647  nnecl  8652  nnawordi  8660  nnmword  8672  nnawordex  8676  nnaordex  8677  oaabslem  8686  oaabs  8687  oaabs2  8688  omabslem  8689  omabs  8690  nnneo  8694  nneob  8695  naddoa  8741  omnaddcl  8742  dif1ennn  9202  findcard2  9205  onfin2  9269  nndomo  9270  findcard3  9319  findcard3OLD  9320  dffi3  9472  card2inf  9596  elom3  9689  cantnfp1lem3  9721  cnfcomlem  9740  cnfcom  9741  cnfcom3  9745  ttrcltr  9757  ttrclselem1  9766  ttrclselem2  9767  finnum  9989  cardnn  10004  nnsdomel  10031  harsucnn  10039  nnadjuALT  10240  ficardun2  10243  ackbij1lem15  10274  ackbij2lem2  10280  ackbij2lem3  10281  ackbij2  10283  fin23lem22  10368  isf32lem5  10398  fin1a2lem4  10444  fin1a2lem9  10449  pwfseqlem3  10701  winainflem  10734  wunr1om  10760  tskr1om  10808  grothomex  10870  pion  10920  om2uzlt2i  13993  madefi  27951  oldfi  27952  precsexlem3  28234  precsexlem4  28235  precsexlem5  28236  om2noseqlt  28306  om2noseqlt2  28307  zs12bday  28425  constrfin  33788  constrextdg2lem  33790  bnj168  34745  satfvsuc  35367  satf0suc  35382  sat1el2xp  35385  fmlasuc0  35390  elhf2  36177  findreccl  36455  rdgeqoa  37372  exrecfnlem  37381  finxpreclem4  37396  finxpreclem6  37398  harinf  43051  onexoegt  43261  oaabsb  43312  nnoeomeqom  43330  cantnfub  43339  dflim5  43347  onmcl  43349  omabs2  43350  tfsconcat0b  43364  naddcnffo  43382  naddonnn  43413  naddwordnexlem0  43414  naddwordnexlem3  43417  oawordex3  43418  naddwordnexlem4  43419  omssrncard  43558  nna1iscard  43563