Theorem nnon 7881

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Oncon0 6361  ωcom 7875

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916  df-om 7876

This theorem is used by:  nnoni  7882  nnord  7883  peano4  7902  findsg  7907  onasuc  8529  onmsuc  8530  nna0  8606  nnm0  8607  nnasuc  8608  nnmsuc  8609  nnesuc  8610  nnecl  8615  nnawordi  8623  nnmword  8635  nnawordex  8639  nnaordex  8640  oaabslem  8649  oaabs  8650  oaabs2  8651  omabslem  8652  omabs  8653  nnneo  8657  nneob  8658  naddoa  8705  omnaddcl  8706  dif1ennn  9171  findcard2  9173  onfin2  9225  nndomo  9226  findcard3  9267  dffi3  9416  card2inf  9542  elom3  9642  cantnfp1lem3  9674  cnfcomlem  9693  cnfcom  9694  cnfcom3  9698  ttrcltr  9710  ttrclselem1  9719  ttrclselem2  9720  elhf2  9903  finnum  10022  cardnn  10037  nnsdomel  10064  harsucnn  10072  nnadjuALT  10270  ficardun2  10273  ackbij1lem15  10304  ackbij2lem2  10310  ackbij2lem3  10311  ackbij2  10313  fin23lem22  10398  isf32lem5  10428  fin1a2lem4  10474  fin1a2lem9  10479  pwfseqlem3  10738  winainflem  10771  wunr1om  10797  tskr1om  10845  grothomex  10907  pion  10957  om2uzlt2i  14087  madefi  28292  oldfi  28293  precsexlem3  28588  precsexlem4  28589  precsexlem5  28590  om2noseqlt  28678  om2noseqlt2  28679  constrfin  34371  constrextdg2lem  34373  constrext2chnlem  34375  constrfiss  34376  constrllcllem  34377  constrlccllem  34378  constrcccllem  34379  constrcn  34385  constrcjcl  34393  bnj168  35354  fineqvnttrclselem1  35772  fineqvnttrclselem2  35773  fineqvnttrclse  35775  kardnnfi  35820  satfvsuc  36105  satf0suc  36120  sat1el2xp  36123  fmlasuc0  36128  findreccl  37221  ttctr  37261  ttcmin  37264  dfttc2g  37274  rdgeqoa  38273  exrecfnlem  38282  finxpreclem4  38297  finxpreclem6  38299  harinf  44020  onexoegt  44230  oaabsb  44280  nnoeomeqom  44298  cantnfub  44307  dflim5  44315  onmcl  44317  omabs2  44318  tfsconcat0b  44332  naddcnffo  44350  naddonnn  44381  naddwordnexlem0  44382  naddwordnexlem3  44385  oawordex3  44386  naddwordnexlem4  44387  omssrncard  44525  nna1iscard  44530  hashnnsuc  45988  hashnnm  45989  hashnnltb  45991