Theorem eloni 6327

Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
eloni	⊢ (𝐴 ∈ On → Ord 𝐴)

Proof of Theorem eloni

Step	Hyp	Ref	Expression
1		elong 6325	. 2 ⊢ (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
2	1	ibi 267	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6316  Oncon0 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3432  df-ss 3907  df-uni 4852  df-tr 5194  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321

This theorem is referenced by:  onelon  6342  onin  6348  ontri1  6351  onfr  6356  onelpss  6357  onsseleq  6358  onelss  6359  oneltri  6360  ontr1  6364  ontr2  6365  ordunidif  6367  on0eln0  6374  ordsssuc  6408  onsssuc  6409  onnbtwn  6413  onunel  6424  suc11  6426  onun2  6427  ontr  6428  onordi  6430  onssneli  6434  epweon  7722  epweonALT  7723  ordeleqon  7729  onss  7732  sucexeloni  7756  onpwsuc  7760  onpsssuc  7763  onsucmin  7765  ordunpr  7770  ordunisuc  7776  onsucuni2  7778  onuniorsuc  7781  ordunisuc2  7788  ordzsl  7789  onzsl  7790  nlimon  7795  tfinds  7804  tfindsg2  7806  nnord  7818  poseq  8101  soseq  8102  onfununi  8274  smo11  8297  smoord  8298  smoword  8299  smogt  8300  tfrlem1  8308  tfrlem9a  8318  tfrlem15  8324  tz7.44-2  8339  tz7.48lem  8373  ord3  8413  oe0m1  8449  oaordi  8474  oaord  8475  oacan  8476  oawordri  8478  oalimcl  8488  oaass  8489  omord2  8495  omcan  8497  omwordi  8499  omword1  8501  omword2  8502  om00  8503  omlimcl  8506  omass  8508  omeulem2  8511  omopth2  8512  oen0  8515  oeord  8517  oecan  8518  oewordi  8520  oeworde  8522  oelimcl  8529  oeeulem  8530  oeeui  8531  nnarcl  8545  nnawordi  8550  nnawordex  8566  oaabs2  8578  omabs  8580  omsmo  8587  cofonr  8603  naddcllem  8605  naddsuc2  8630  omxpenlem  9009  infensuc  9086  dif1enlem  9087  nndomog  9140  onomeneq  9141  ordiso  9424  ordtypelem2  9427  hartogslem1  9450  cantnflt  9584  cantnfp1lem3  9592  cantnfp1  9593  oemapso  9594  oemapvali  9596  cantnflem1d  9600  cantnflem1  9601  cantnf  9605  oemapwe  9606  cantnffval2  9607  cnfcom  9612  r111  9690  r1ordg  9693  rankonidlem  9743  bndrank  9756  r1pw  9760  r1pwALT  9761  rankbnd2  9784  tcrank  9799  cardprclem  9894  carduni  9896  cardmin2  9914  infxpenlem  9926  alephdom  9994  alephdom2  10000  cardaleph  10002  iscard3  10006  alephfp  10021  dfac12lem1  10057  dfac12lem2  10058  dfac12lem3  10059  cflim2  10176  cofsmo  10182  cfsmolem  10183  coftr  10186  cfcof  10187  fin67  10308  hsmexlem5  10343  zorn2lem6  10414  ttukeylem3  10424  ttukeylem5  10426  ttukeylem6  10427  ttukeylem7  10428  winainflem  10607  r1limwun  10650  r1wunlim  10651  tsksuc  10676  inar1  10689  gruina  10732  grur1a  10733  grur1  10734  nodmord  27631  noextendseq  27645  noextenddif  27646  nosupno  27681  nosupbday  27683  nosupres  27685  noinfno  27696  noinfbday  27698  noinfres  27700  noetasuplem4  27714  noetainflem4  27718  newbday  27908  oldfib  28383  fineqvnttrclse  35284  dfrdg2  35991  ontgval  36629  ontgsucval  36630  onsuctopon  36632  onintopssconn  36638  onsuct0  36639  sucneqond  37695  onsucuni3  37697  aomclem4  43503  aomclem5  43504  onintunirab  43673  omlimcl2  43688  onelord  43697  ordeldifsucon  43705  ordeldif1o  43706  onsucss  43712  onsucf1olem  43716  onov0suclim  43720  oe0rif  43731  onsucwordi  43734  oege1  43752  cantnfresb  43770  omabs2  43778  ordsssucb  43781  tfsconcatlem  43782  tfsconcatfv2  43786  tfsconcatrn  43788  tfsconcatb0  43790  tfsconcat0b  43792  tfsconcatrev  43794  onsucunipr  43818  oaun3lem1  43820  oaun3lem2  43821  nadd1suc  43838  naddgeoa  43840  oaltom  43850  omltoe  43852  nlimsuc  43886  dfsucon  43968  minregex  43979  onfrALTlem3  44989  onfrALTlem2  44991  onfrALTlem3VD  45331  onfrALTlem2VD  45333  onsetreclem3  50194