Theorem eloni 6374

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

Syntax hints:   → wi 4   ∈ wcel 2106  Ord word 6363  Oncon0 6364

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368

This theorem is referenced by:  onelon  6389  onin  6395  ontri1  6398  onfr  6403  onelpss  6404  onsseleq  6405  onelss  6406  ontr1  6410  ontr2  6411  ordunidif  6413  on0eln0  6420  ordsssuc  6453  onsssuc  6454  onnbtwn  6458  onunel  6469  suc11  6471  onun2  6472  ontr  6473  onordi  6475  onssneli  6480  epweon  7764  epweonALT  7765  ordeleqon  7771  onss  7774  sucexeloni  7799  ordsucOLD  7804  onpwsuc  7806  onpsssuc  7809  onsucmin  7811  ordunpr  7816  ordunisuc  7822  onsucuni2  7824  onuniorsuc  7827  ordunisuc2  7835  ordzsl  7836  onzsl  7837  nlimon  7842  tfinds  7851  tfindsg2  7853  nnord  7865  poseq  8146  soseq  8147  onfununi  8343  smo11  8366  smoord  8367  smoword  8368  smogt  8369  tfrlem1  8378  tfrlem9a  8388  tfrlem15  8394  tz7.44-2  8409  tz7.48lem  8443  ord3  8485  oe0m1  8523  oaordi  8548  oaord  8549  oacan  8550  oawordri  8552  oalimcl  8562  oaass  8563  omord2  8569  omcan  8571  omwordi  8573  omword1  8575  omword2  8576  om00  8577  omlimcl  8580  omass  8582  omeulem2  8585  omopth2  8586  oen0  8588  oeord  8590  oecan  8591  oewordi  8593  oeworde  8595  oelimcl  8602  oeeulem  8603  oeeui  8604  nnarcl  8618  nnawordi  8623  nnawordex  8639  oaabs2  8650  omabs  8652  omsmo  8659  cofonr  8675  naddcllem  8677  omxpenlem  9075  infensuc  9157  dif1enlem  9158  nndomog  9218  nndomogOLD  9228  onomeneq  9230  onomeneqOLD  9231  ordiso  9513  ordtypelem2  9516  hartogslem1  9539  cantnflt  9669  cantnfp1lem3  9677  cantnfp1  9678  oemapso  9679  oemapvali  9681  cantnflem1d  9685  cantnflem1  9686  cantnf  9690  oemapwe  9691  cantnffval2  9692  cnfcom  9697  r111  9772  r1ordg  9775  rankonidlem  9825  bndrank  9838  r1pw  9842  r1pwALT  9843  rankbnd2  9866  tcrank  9881  cardprclem  9976  carduni  9978  cardmin2  9996  infxpenlem  10010  alephdom  10078  alephdom2  10084  cardaleph  10086  iscard3  10090  alephfp  10105  dfac12lem1  10140  dfac12lem2  10141  dfac12lem3  10142  cflim2  10260  cofsmo  10266  cfsmolem  10267  coftr  10270  cfcof  10271  fin67  10392  hsmexlem5  10427  zorn2lem6  10498  ttukeylem3  10508  ttukeylem5  10510  ttukeylem6  10511  ttukeylem7  10512  winainflem  10690  r1limwun  10733  r1wunlim  10734  tsksuc  10759  inar1  10772  gruina  10815  grur1a  10816  grur1  10817  nodmord  27380  noextendseq  27394  noextenddif  27395  nosupno  27430  nosupbday  27432  nosupres  27434  noinfno  27445  noinfbday  27447  noinfres  27449  noetasuplem4  27463  noetainflem4  27467  newbday  27621  dfrdg2  35059  ontgval  35619  ontgsucval  35620  onsuctopon  35622  onintopssconn  35628  onsuct0  35629  sucneqond  36549  onsucuni3  36551  aomclem4  42101  aomclem5  42102  onintunirab  42278  omlimcl2  42293  onelord  42302  oneltri  42309  ordeldifsucon  42311  ordeldif1o  42312  onsucss  42318  onsucf1olem  42322  onov0suclim  42326  oe0rif  42337  onsucwordi  42340  oege1  42358  cantnfresb  42376  omabs2  42384  ordsssucb  42387  tfsconcatlem  42388  tfsconcatfv2  42392  tfsconcatrn  42394  tfsconcatb0  42396  tfsconcat0b  42398  tfsconcatrev  42400  onsucunipr  42424  oaun3lem1  42426  oaun3lem2  42427  nadd1suc  42444  naddsuc2  42445  naddgeoa  42447  oaltom  42458  omltoe  42460  nlimsuc  42494  dfsucon  42576  minregex  42587  onfrALTlem3  43607  onfrALTlem2  43609  onfrALTlem3VD  43950  onfrALTlem2VD  43952  onsetreclem3  47840