MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eloni Unicode version

Theorem eloni 4532
Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
eloni  |-  ( A  e.  On  ->  Ord  A )

Proof of Theorem eloni
StepHypRef Expression
1 elong 4530 . 2  |-  ( A  e.  On  ->  ( A  e.  On  <->  Ord  A ) )
21ibi 233 1  |-  ( A  e.  On  ->  Ord  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   Ord word 4521   Oncon0 4522
This theorem is referenced by:  elon2  4533  onelon  4547  onin  4553  ontri1  4556  onfr  4561  onelpss  4562  onsseleq  4563  onelss  4564  ontr1  4568  ontr2  4569  ordunidif  4570  on0eln0  4577  ordsssuc  4608  onsssuc  4609  onnbtwn  4613  suc11  4625  onordi  4626  onssneli  4631  ordon  4703  ordeleqon  4709  onss  4711  ordsuc  4734  onpwsuc  4736  onpsssuc  4739  onsucmin  4741  ordunpr  4746  ordunisuc  4752  onsucuni2  4754  onuninsuci  4760  ordunisuc2  4764  ordzsl  4765  onzsl  4766  nlimon  4771  tfinds  4779  tfindsg2  4781  nnord  4793  onfununi  6539  smo11  6562  smoord  6563  smoword  6564  smogt  6565  tfrlem9a  6583  tfrlem15  6589  tz7.44-2  6601  tz7.48lem  6634  oe0m1  6701  oaordi  6725  oaord  6726  oacan  6727  oawordri  6729  oalimcl  6739  oaass  6740  omord2  6746  omcan  6748  omwordi  6750  omword1  6752  omword2  6753  om00  6754  omlimcl  6757  omass  6759  omeulem2  6762  omopth2  6763  oen0  6765  oeord  6767  oecan  6768  oewordi  6770  oeworde  6772  oelimcl  6779  oeeulem  6780  oeeui  6781  nnarcl  6795  nnawordi  6800  nnawordex  6816  oaabs2  6824  omabs  6826  omsmo  6833  omxpenlem  7145  infensuc  7221  onomeneq  7232  ordiso  7418  ordtypelem2  7421  hartogslem1  7444  cantnflt  7560  cantnfp1lem3  7569  cantnfp1  7570  oemapso  7571  oemapvali  7573  cantnflem1d  7577  cantnflem1  7578  cantnf  7582  oemapwe  7583  cantnffval2  7584  cnfcom  7590  r111  7634  r1ordg  7637  rankonidlem  7687  bndrank  7700  r1pw  7704  r1pwOLD  7705  rankbnd2  7728  tcrank  7741  cardprclem  7799  carduni  7801  cardmin2  7818  infxpenlem  7828  alephdom  7895  alephdom2  7901  cardaleph  7903  iscard3  7907  alephfp  7922  dfac12lem1  7956  dfac12lem2  7957  dfac12lem3  7958  cflim2  8076  cofsmo  8082  cfsmolem  8083  coftr  8086  cfcof  8087  fin67  8208  hsmexlem5  8243  zorn2lem6  8314  ttukeylem3  8324  ttukeylem5  8326  ttukeylem6  8327  ttukeylem7  8328  winainflem  8501  r1limwun  8544  r1wunlim  8545  tsksuc  8570  inar1  8583  gruina  8626  grur1a  8627  grur1  8628  dfrdg2  25176  poseq  25277  soseq  25278  nodmord  25331  nodenselem5  25363  nofulllem5  25384  ontgval  25895  ontgsucval  25896  onsuctopon  25898  onintopsscon  25904  onsuct0  25905  aomclem4  26823  aomclem5  26824  onfrALTlem3  27973  onfrALTlem2  27975  onfrALTlem3VD  28340  onfrALTlem2VD  28342
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-rex 2655  df-v 2901  df-in 3270  df-ss 3277  df-uni 3958  df-tr 4244  df-po 4444  df-so 4445  df-fr 4482  df-we 4484  df-ord 4525  df-on 4526
  Copyright terms: Public domain W3C validator