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

Theorem eloni 4874
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 4872 . 2  |-  ( A  e.  On  ->  ( A  e.  On  <->  Ord  A ) )
21ibi 241 1  |-  ( A  e.  On  ->  Ord  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   Ord word 4863   Oncon0 4864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797  df-v 3095  df-in 3465  df-ss 3472  df-uni 4231  df-tr 4527  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868
This theorem is referenced by:  elon2  4875  onelon  4889  onin  4895  ontri1  4898  onfr  4903  onelpss  4904  onsseleq  4905  onelss  4906  ontr1  4910  ontr2  4911  ordunidif  4912  on0eln0  4919  ordsssuc  4950  onsssuc  4951  onnbtwn  4955  suc11  4967  onordi  4968  onssneli  4973  ordon  6599  ordeleqon  6605  onss  6607  ordsuc  6630  onpwsuc  6632  onpsssuc  6635  onsucmin  6637  ordunpr  6642  ordunisuc  6648  onsucuni2  6650  onuninsuci  6656  ordunisuc2  6660  ordzsl  6661  onzsl  6662  nlimon  6667  tfinds  6675  tfindsg2  6677  nnord  6689  onfununi  7010  smo11  7033  smoord  7034  smoword  7035  smogt  7036  tfrlem1  7043  tfrlem9a  7053  tfrlem15  7059  tz7.44-2  7071  tz7.48lem  7104  oe0m1  7169  oaordi  7193  oaord  7194  oacan  7195  oawordri  7197  oalimcl  7207  oaass  7208  omord2  7214  omcan  7216  omwordi  7218  omword1  7220  omword2  7221  om00  7222  omlimcl  7225  omass  7227  omeulem2  7230  omopth2  7231  oen0  7233  oeord  7235  oecan  7236  oewordi  7238  oeworde  7240  oelimcl  7247  oeeulem  7248  oeeui  7249  nnarcl  7263  nnawordi  7268  nnawordex  7284  oaabs2  7292  omabs  7294  omsmo  7301  omxpenlem  7616  infensuc  7693  onomeneq  7705  ordiso  7939  ordtypelem2  7942  hartogslem1  7965  cantnflt  8089  cantnfp1lem3  8097  cantnfp1  8098  oemapso  8099  oemapvali  8101  cantnflem1d  8105  cantnflem1  8106  cantnf  8110  oemapwe  8111  cantnffval2  8112  cantnfltOLD  8119  cantnfp1lem3OLD  8123  cantnfp1OLD  8124  cantnflem1dOLD  8128  cantnflem1OLD  8129  cantnfOLD  8132  oemapweOLD  8133  cantnffval2OLD  8134  cnfcom  8142  cnfcomOLD  8150  r111  8191  r1ordg  8194  rankonidlem  8244  bndrank  8257  r1pw  8261  r1pwOLD  8262  rankbnd2  8285  tcrank  8300  cardprclem  8358  carduni  8360  cardmin2  8377  infxpenlem  8389  alephdom  8460  alephdom2  8466  cardaleph  8468  iscard3  8472  alephfp  8487  dfac12lem1  8521  dfac12lem2  8522  dfac12lem3  8523  cflim2  8641  cofsmo  8647  cfsmolem  8648  coftr  8651  cfcof  8652  fin67  8773  hsmexlem5  8808  zorn2lem6  8879  ttukeylem3  8889  ttukeylem5  8891  ttukeylem6  8892  ttukeylem7  8893  winainflem  9069  r1limwun  9112  r1wunlim  9113  tsksuc  9138  inar1  9151  gruina  9194  grur1a  9195  grur1  9196  dfrdg2  29196  poseq  29301  soseq  29302  nodmord  29381  nodenselem5  29413  nofulllem5  29434  ontgval  29864  ontgsucval  29865  onsuctopon  29867  onintopsscon  29873  onsuct0  29874  aomclem4  30971  aomclem5  30972  onfrALTlem3  33024  onfrALTlem2  33026  onfrALTlem3VD  33395  onfrALTlem2VD  33397
  Copyright terms: Public domain W3C validator