Theorem eloni 6359

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

Syntax hints:   → wi 4   ∈ wcel 2145  Ord word 6348  Oncon0 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-v 3459  df-ss 3924  df-uni 4868  df-tr 5212  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6352  df-on 6353

This theorem is referenced by:  onelon  6374  onin  6381  ontri1  6384  onfr  6389  onelpss  6390  onsseleq  6391  onelss  6392  oneltri  6393  ontr1  6397  ontr2  6398  ordunidif  6400  on0eln0  6407  ordsssuc  6441  onsssuc  6442  onnbtwn  6446  onunel  6457  suc11  6459  onun2  6460  ontr  6461  onordi  6463  onssneli  6467  epweon  7762  epweonALT  7763  ordeleqon  7769  onss  7772  sucexeloni  7796  onpwsuc  7800  onpsssuc  7803  onsucmin  7805  ordunpr  7810  ordunisuc  7816  onsucuni2  7818  onuniorsuc  7821  ordunisuc2  7828  ordzsl  7829  onzsl  7830  nlimon  7835  tfinds  7844  tfindsg2  7846  nnord  7858  poseq  8142  soseq  8143  onfununi  8316  smo11  8339  smoord  8340  smoword  8341  smogt  8342  tfrlem1  8350  tfrlem9a  8361  tfrlem15  8367  tz7.44-2  8382  tz7.48lem  8416  ord3  8457  oe0m1  8494  oaordi  8519  oaord  8520  oacan  8521  oawordri  8523  oalimcl  8533  oaass  8534  omord2  8540  omcan  8542  omwordi  8544  omword1  8546  omword2  8547  om00  8548  omlimcl  8551  omass  8553  omeulem2  8556  omopth2  8557  oen0  8560  oeord  8562  oecan  8563  oewordi  8565  oeworde  8567  oelimcl  8574  oeeulem  8575  oeeui  8576  nnarcl  8590  nnawordi  8595  nnawordex  8611  oaabs2  8623  omabs  8625  omsmo  8632  cofonr  8648  naddcllem  8650  naddsuc2  8676  omxpenlem  9054  infensuc  9131  dif1enlem  9132  nndomog  9185  onomeneq  9186  ordiso  9466  ordtypelem2  9469  hartogslem1  9492  cantnflt  9629  cantnfp1lem3  9637  cantnfp1  9638  oemapso  9639  oemapvali  9641  cantnflem1d  9645  cantnflem1  9646  cantnf  9650  oemapwe  9651  cantnffval2  9652  cnfcom  9657  r111  9735  r1ordg  9738  rankonidlem  9788  bndrank  9801  r1pw  9805  r1pwALT  9806  rankbnd2  9829  tcrank  9844  cardprclem  9953  carduni  9955  cardmin2  9973  infxpenlem  9985  alephdom  10053  alephdom2  10059  cardaleph  10061  iscard3  10065  alephfp  10080  dfac12lem1  10115  dfac12lem2  10116  dfac12lem3  10117  cflim2  10235  cofsmo  10241  cfsmolem  10242  coftr  10245  cfcof  10246  fin67  10367  hsmexlem5  10402  zorn2lem6  10473  ttukeylem3  10483  ttukeylem5  10485  ttukeylem6  10486  ttukeylem7  10487  winainflem  10666  r1limwun  10709  r1wunlim  10710  tsksuc  10735  inar1  10748  gruina  10791  grur1a  10792  grur1  10793  nodmord  27771  noextendseq  27785  noextenddif  27786  nosupno  27821  nosupbday  27823  nosupres  27825  noinfno  27836  noinfbday  27838  noinfres  27840  noetasuplem4  27854  noetainflem4  27858  newbday  28049  oldfib  28524  fineqvnttrclse  35427  dfrdg2  36151  nmulprop  36548  ontgval  36799  ontgsucval  36800  onsuctopon  36802  onintopssconn  36808  onsuct0  36809  sucneqond  37866  onsucuni3  37868  aomclem4  43641  aomclem5  43642  onintunirab  43811  omlimcl2  43826  onelord  43835  ordeldifsucon  43843  ordeldif1o  43844  onsucss  43850  onsucf1olem  43854  onov0suclim  43858  oe0rif  43869  onsucwordi  43872  oege1  43890  cantnfresb  43908  omabs2  43916  ordsssucb  43919  tfsconcatlem  43920  tfsconcatfv2  43924  tfsconcatrn  43926  tfsconcatb0  43928  tfsconcat0b  43930  tfsconcatrev  43932  onsucunipr  43956  oaun3lem1  43958  oaun3lem2  43959  nadd1suc  43976  naddgeoa  43978  oaltom  43988  omltoe  43990  nlimsuc  44024  dfsucon  44106  minregex  44117  onfrALTlem3  45112  onfrALTlem2  45114  onfrALTlem3VD  45454  onfrALTlem2VD  45456  onsetreclem3  50337