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

Theorem eloni 4555
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 4553 . 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 1721   Ord word 4544   Oncon0 4545
This theorem is referenced by:  elon2  4556  onelon  4570  onin  4576  ontri1  4579  onfr  4584  onelpss  4585  onsseleq  4586  onelss  4587  ontr1  4591  ontr2  4592  ordunidif  4593  on0eln0  4600  ordsssuc  4631  onsssuc  4632  onnbtwn  4636  suc11  4648  onordi  4649  onssneli  4654  ordon  4726  ordeleqon  4732  onss  4734  ordsuc  4757  onpwsuc  4759  onpsssuc  4762  onsucmin  4764  ordunpr  4769  ordunisuc  4775  onsucuni2  4777  onuninsuci  4783  ordunisuc2  4787  ordzsl  4788  onzsl  4789  nlimon  4794  tfinds  4802  tfindsg2  4804  nnord  4816  onfununi  6566  smo11  6589  smoord  6590  smoword  6591  smogt  6592  tfrlem9a  6610  tfrlem15  6616  tz7.44-2  6628  tz7.48lem  6661  oe0m1  6728  oaordi  6752  oaord  6753  oacan  6754  oawordri  6756  oalimcl  6766  oaass  6767  omord2  6773  omcan  6775  omwordi  6777  omword1  6779  omword2  6780  om00  6781  omlimcl  6784  omass  6786  omeulem2  6789  omopth2  6790  oen0  6792  oeord  6794  oecan  6795  oewordi  6797  oeworde  6799  oelimcl  6806  oeeulem  6807  oeeui  6808  nnarcl  6822  nnawordi  6827  nnawordex  6843  oaabs2  6851  omabs  6853  omsmo  6860  omxpenlem  7172  infensuc  7248  onomeneq  7259  ordiso  7445  ordtypelem2  7448  hartogslem1  7471  cantnflt  7587  cantnfp1lem3  7596  cantnfp1  7597  oemapso  7598  oemapvali  7600  cantnflem1d  7604  cantnflem1  7605  cantnf  7609  oemapwe  7610  cantnffval2  7611  cnfcom  7617  r111  7661  r1ordg  7664  rankonidlem  7714  bndrank  7727  r1pw  7731  r1pwOLD  7732  rankbnd2  7755  tcrank  7768  cardprclem  7826  carduni  7828  cardmin2  7845  infxpenlem  7855  alephdom  7922  alephdom2  7928  cardaleph  7930  iscard3  7934  alephfp  7949  dfac12lem1  7983  dfac12lem2  7984  dfac12lem3  7985  cflim2  8103  cofsmo  8109  cfsmolem  8110  coftr  8113  cfcof  8114  fin67  8235  hsmexlem5  8270  zorn2lem6  8341  ttukeylem3  8351  ttukeylem5  8353  ttukeylem6  8354  ttukeylem7  8355  winainflem  8528  r1limwun  8571  r1wunlim  8572  tsksuc  8597  inar1  8610  gruina  8653  grur1a  8654  grur1  8655  dfrdg2  25370  poseq  25471  soseq  25472  nodmord  25525  nodenselem5  25557  nofulllem5  25578  ontgval  26089  ontgsucval  26090  onsuctopon  26092  onintopsscon  26098  onsuct0  26099  aomclem4  27026  aomclem5  27027  onfrALTlem3  28345  onfrALTlem2  28347  onfrALTlem3VD  28712  onfrALTlem2VD  28714
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ral 2675  df-rex 2676  df-v 2922  df-in 3291  df-ss 3298  df-uni 3980  df-tr 4267  df-po 4467  df-so 4468  df-fr 4505  df-we 4507  df-ord 4548  df-on 4549
  Copyright terms: Public domain W3C validator