Theorem eloni 6335

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 6333	. 2 ⊢ (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
2	1	ibi 267	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6324  Oncon0 6325

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 3444  df-ss 3920  df-uni 4866  df-tr 5208  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329

This theorem is referenced by:  onelon  6350  onin  6356  ontri1  6359  onfr  6364  onelpss  6365  onsseleq  6366  onelss  6367  oneltri  6368  ontr1  6372  ontr2  6373  ordunidif  6375  on0eln0  6382  ordsssuc  6416  onsssuc  6417  onnbtwn  6421  onunel  6432  suc11  6434  onun2  6435  ontr  6436  onordi  6438  onssneli  6442  epweon  7730  epweonALT  7731  ordeleqon  7737  onss  7740  sucexeloni  7764  onpwsuc  7768  onpsssuc  7771  onsucmin  7773  ordunpr  7778  ordunisuc  7784  onsucuni2  7786  onuniorsuc  7789  ordunisuc2  7796  ordzsl  7797  onzsl  7798  nlimon  7803  tfinds  7812  tfindsg2  7814  nnord  7826  poseq  8110  soseq  8111  onfununi  8283  smo11  8306  smoord  8307  smoword  8308  smogt  8309  tfrlem1  8317  tfrlem9a  8327  tfrlem15  8333  tz7.44-2  8348  tz7.48lem  8382  ord3  8422  oe0m1  8458  oaordi  8483  oaord  8484  oacan  8485  oawordri  8487  oalimcl  8497  oaass  8498  omord2  8504  omcan  8506  omwordi  8508  omword1  8510  omword2  8511  om00  8512  omlimcl  8515  omass  8517  omeulem2  8520  omopth2  8521  oen0  8524  oeord  8526  oecan  8527  oewordi  8529  oeworde  8531  oelimcl  8538  oeeulem  8539  oeeui  8540  nnarcl  8554  nnawordi  8559  nnawordex  8575  oaabs2  8587  omabs  8589  omsmo  8596  cofonr  8612  naddcllem  8614  naddsuc2  8639  omxpenlem  9018  infensuc  9095  dif1enlem  9096  nndomog  9149  onomeneq  9150  ordiso  9433  ordtypelem2  9436  hartogslem1  9459  cantnflt  9593  cantnfp1lem3  9601  cantnfp1  9602  oemapso  9603  oemapvali  9605  cantnflem1d  9609  cantnflem1  9610  cantnf  9614  oemapwe  9615  cantnffval2  9616  cnfcom  9621  r111  9699  r1ordg  9702  rankonidlem  9752  bndrank  9765  r1pw  9769  r1pwALT  9770  rankbnd2  9793  tcrank  9808  cardprclem  9903  carduni  9905  cardmin2  9923  infxpenlem  9935  alephdom  10003  alephdom2  10009  cardaleph  10011  iscard3  10015  alephfp  10030  dfac12lem1  10066  dfac12lem2  10067  dfac12lem3  10068  cflim2  10185  cofsmo  10191  cfsmolem  10192  coftr  10195  cfcof  10196  fin67  10317  hsmexlem5  10352  zorn2lem6  10423  ttukeylem3  10433  ttukeylem5  10435  ttukeylem6  10436  ttukeylem7  10437  winainflem  10616  r1limwun  10659  r1wunlim  10660  tsksuc  10685  inar1  10698  gruina  10741  grur1a  10742  grur1  10743  nodmord  27633  noextendseq  27647  noextenddif  27648  nosupno  27683  nosupbday  27685  nosupres  27687  noinfno  27698  noinfbday  27700  noinfres  27702  noetasuplem4  27716  noetainflem4  27720  newbday  27910  oldfib  28385  fineqvnttrclse  35299  dfrdg2  36006  ontgval  36644  ontgsucval  36645  onsuctopon  36647  onintopssconn  36653  onsuct0  36654  sucneqond  37614  onsucuni3  37616  aomclem4  43408  aomclem5  43409  onintunirab  43578  omlimcl2  43593  onelord  43602  ordeldifsucon  43610  ordeldif1o  43611  onsucss  43617  onsucf1olem  43621  onov0suclim  43625  oe0rif  43636  onsucwordi  43639  oege1  43657  cantnfresb  43675  omabs2  43683  ordsssucb  43686  tfsconcatlem  43687  tfsconcatfv2  43691  tfsconcatrn  43693  tfsconcatb0  43695  tfsconcat0b  43697  tfsconcatrev  43699  onsucunipr  43723  oaun3lem1  43725  oaun3lem2  43726  nadd1suc  43743  naddgeoa  43745  oaltom  43755  omltoe  43757  nlimsuc  43791  dfsucon  43873  minregex  43884  onfrALTlem3  44894  onfrALTlem2  44896  onfrALTlem3VD  45236  onfrALTlem2VD  45238  onsetreclem3  50060