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

Theorem eloni 4593
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 4591 . 2  |-  ( A  e.  On  ->  ( A  e.  On  <->  Ord  A ) )
21ibi 234 1  |-  ( A  e.  On  ->  Ord  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   Ord word 4582   Oncon0 4583
This theorem is referenced by:  elon2  4594  onelon  4608  onin  4614  ontri1  4617  onfr  4622  onelpss  4623  onsseleq  4624  onelss  4625  ontr1  4629  ontr2  4630  ordunidif  4631  on0eln0  4638  ordsssuc  4670  onsssuc  4671  onnbtwn  4675  suc11  4687  onordi  4688  onssneli  4693  ordon  4765  ordeleqon  4771  onss  4773  ordsuc  4796  onpwsuc  4798  onpsssuc  4801  onsucmin  4803  ordunpr  4808  ordunisuc  4814  onsucuni2  4816  onuninsuci  4822  ordunisuc2  4826  ordzsl  4827  onzsl  4828  nlimon  4833  tfinds  4841  tfindsg2  4843  nnord  4855  onfununi  6605  smo11  6628  smoord  6629  smoword  6630  smogt  6631  tfrlem9a  6649  tfrlem15  6655  tz7.44-2  6667  tz7.48lem  6700  oe0m1  6767  oaordi  6791  oaord  6792  oacan  6793  oawordri  6795  oalimcl  6805  oaass  6806  omord2  6812  omcan  6814  omwordi  6816  omword1  6818  omword2  6819  om00  6820  omlimcl  6823  omass  6825  omeulem2  6828  omopth2  6829  oen0  6831  oeord  6833  oecan  6834  oewordi  6836  oeworde  6838  oelimcl  6845  oeeulem  6846  oeeui  6847  nnarcl  6861  nnawordi  6866  nnawordex  6882  oaabs2  6890  omabs  6892  omsmo  6899  omxpenlem  7211  infensuc  7287  onomeneq  7298  ordiso  7487  ordtypelem2  7490  hartogslem1  7513  cantnflt  7629  cantnfp1lem3  7638  cantnfp1  7639  oemapso  7640  oemapvali  7642  cantnflem1d  7646  cantnflem1  7647  cantnf  7651  oemapwe  7652  cantnffval2  7653  cnfcom  7659  r111  7703  r1ordg  7706  rankonidlem  7756  bndrank  7769  r1pw  7773  r1pwOLD  7774  rankbnd2  7797  tcrank  7810  cardprclem  7868  carduni  7870  cardmin2  7887  infxpenlem  7897  alephdom  7964  alephdom2  7970  cardaleph  7972  iscard3  7976  alephfp  7991  dfac12lem1  8025  dfac12lem2  8026  dfac12lem3  8027  cflim2  8145  cofsmo  8151  cfsmolem  8152  coftr  8155  cfcof  8156  fin67  8277  hsmexlem5  8312  zorn2lem6  8383  ttukeylem3  8393  ttukeylem5  8395  ttukeylem6  8396  ttukeylem7  8397  winainflem  8570  r1limwun  8613  r1wunlim  8614  tsksuc  8639  inar1  8652  gruina  8695  grur1a  8696  grur1  8697  dfrdg2  25425  poseq  25530  soseq  25531  nodmord  25610  nodenselem5  25642  nofulllem5  25663  ontgval  26183  ontgsucval  26184  onsuctopon  26186  onintopsscon  26192  onsuct0  26193  aomclem4  27134  aomclem5  27135  onfrALTlem3  28692  onfrALTlem2  28694  onfrALTlem3VD  29061  onfrALTlem2VD  29063
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-v 2960  df-in 3329  df-ss 3336  df-uni 4018  df-tr 4305  df-po 4505  df-so 4506  df-fr 4543  df-we 4545  df-ord 4586  df-on 4587
  Copyright terms: Public domain W3C validator