Theorem eloni 6405

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ord word 6394  Oncon0 6395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-ss 3993  df-uni 4932  df-tr 5284  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399

This theorem is referenced by:  onelon  6420  onin  6426  ontri1  6429  onfr  6434  onelpss  6435  onsseleq  6436  onelss  6437  ontr1  6441  ontr2  6442  ordunidif  6444  on0eln0  6451  ordsssuc  6484  onsssuc  6485  onnbtwn  6489  onunel  6500  suc11  6502  onun2  6503  ontr  6504  onordi  6506  onssneli  6511  epweon  7810  epweonALT  7811  ordeleqon  7817  onss  7820  sucexeloni  7845  ordsucOLD  7850  onpwsuc  7852  onpsssuc  7855  onsucmin  7857  ordunpr  7862  ordunisuc  7868  onsucuni2  7870  onuniorsuc  7873  ordunisuc2  7881  ordzsl  7882  onzsl  7883  nlimon  7888  tfinds  7897  tfindsg2  7899  nnord  7911  poseq  8199  soseq  8200  onfununi  8397  smo11  8420  smoord  8421  smoword  8422  smogt  8423  tfrlem1  8432  tfrlem9a  8442  tfrlem15  8448  tz7.44-2  8463  tz7.48lem  8497  ord3  8539  oe0m1  8577  oaordi  8602  oaord  8603  oacan  8604  oawordri  8606  oalimcl  8616  oaass  8617  omord2  8623  omcan  8625  omwordi  8627  omword1  8629  omword2  8630  om00  8631  omlimcl  8634  omass  8636  omeulem2  8639  omopth2  8640  oen0  8642  oeord  8644  oecan  8645  oewordi  8647  oeworde  8649  oelimcl  8656  oeeulem  8657  oeeui  8658  nnarcl  8672  nnawordi  8677  nnawordex  8693  oaabs2  8705  omabs  8707  omsmo  8714  cofonr  8730  naddcllem  8732  naddsuc2  8757  omxpenlem  9139  infensuc  9221  dif1enlem  9222  nndomog  9279  nndomogOLD  9289  onomeneq  9291  onomeneqOLD  9292  ordiso  9585  ordtypelem2  9588  hartogslem1  9611  cantnflt  9741  cantnfp1lem3  9749  cantnfp1  9750  oemapso  9751  oemapvali  9753  cantnflem1d  9757  cantnflem1  9758  cantnf  9762  oemapwe  9763  cantnffval2  9764  cnfcom  9769  r111  9844  r1ordg  9847  rankonidlem  9897  bndrank  9910  r1pw  9914  r1pwALT  9915  rankbnd2  9938  tcrank  9953  cardprclem  10048  carduni  10050  cardmin2  10068  infxpenlem  10082  alephdom  10150  alephdom2  10156  cardaleph  10158  iscard3  10162  alephfp  10177  dfac12lem1  10213  dfac12lem2  10214  dfac12lem3  10215  cflim2  10332  cofsmo  10338  cfsmolem  10339  coftr  10342  cfcof  10343  fin67  10464  hsmexlem5  10499  zorn2lem6  10570  ttukeylem3  10580  ttukeylem5  10582  ttukeylem6  10583  ttukeylem7  10584  winainflem  10762  r1limwun  10805  r1wunlim  10806  tsksuc  10831  inar1  10844  gruina  10887  grur1a  10888  grur1  10889  nodmord  27716  noextendseq  27730  noextenddif  27731  nosupno  27766  nosupbday  27768  nosupres  27770  noinfno  27781  noinfbday  27783  noinfres  27785  noetasuplem4  27799  noetainflem4  27803  newbday  27958  dfrdg2  35759  ontgval  36397  ontgsucval  36398  onsuctopon  36400  onintopssconn  36406  onsuct0  36407  sucneqond  37331  onsucuni3  37333  aomclem4  43014  aomclem5  43015  onintunirab  43188  omlimcl2  43203  onelord  43212  oneltri  43219  ordeldifsucon  43221  ordeldif1o  43222  onsucss  43228  onsucf1olem  43232  onov0suclim  43236  oe0rif  43247  onsucwordi  43250  oege1  43268  cantnfresb  43286  omabs2  43294  ordsssucb  43297  tfsconcatlem  43298  tfsconcatfv2  43302  tfsconcatrn  43304  tfsconcatb0  43306  tfsconcat0b  43308  tfsconcatrev  43310  onsucunipr  43334  oaun3lem1  43336  oaun3lem2  43337  nadd1suc  43354  naddgeoa  43356  oaltom  43367  omltoe  43369  nlimsuc  43403  dfsucon  43485  minregex  43496  onfrALTlem3  44515  onfrALTlem2  44517  onfrALTlem3VD  44858  onfrALTlem2VD  44860  onsetreclem3  48799