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

Theorem eloni 4734
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 4732 . 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 1756   Ord word 4723   Oncon0 4724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-rex 2726  df-v 2979  df-in 3340  df-ss 3347  df-uni 4097  df-tr 4391  df-po 4646  df-so 4647  df-fr 4684  df-we 4686  df-ord 4727  df-on 4728
This theorem is referenced by:  elon2  4735  onelon  4749  onin  4755  ontri1  4758  onfr  4763  onelpss  4764  onsseleq  4765  onelss  4766  ontr1  4770  ontr2  4771  ordunidif  4772  on0eln0  4779  ordsssuc  4810  onsssuc  4811  onnbtwn  4815  suc11  4827  onordi  4828  onssneli  4833  ordon  6399  ordeleqon  6405  onss  6407  ordsuc  6430  onpwsuc  6432  onpsssuc  6435  onsucmin  6437  ordunpr  6442  ordunisuc  6448  onsucuni2  6450  onuninsuci  6456  ordunisuc2  6460  ordzsl  6461  onzsl  6462  nlimon  6467  tfinds  6475  tfindsg2  6477  nnord  6489  onfununi  6807  smo11  6830  smoord  6831  smoword  6832  smogt  6833  tfrlem1  6840  tfrlem9a  6850  tfrlem15  6856  tz7.44-2  6868  tz7.48lem  6901  oe0m1  6966  oaordi  6990  oaord  6991  oacan  6992  oawordri  6994  oalimcl  7004  oaass  7005  omord2  7011  omcan  7013  omwordi  7015  omword1  7017  omword2  7018  om00  7019  omlimcl  7022  omass  7024  omeulem2  7027  omopth2  7028  oen0  7030  oeord  7032  oecan  7033  oewordi  7035  oeworde  7037  oelimcl  7044  oeeulem  7045  oeeui  7046  nnarcl  7060  nnawordi  7065  nnawordex  7081  oaabs2  7089  omabs  7091  omsmo  7098  omxpenlem  7417  infensuc  7494  onomeneq  7505  ordiso  7735  ordtypelem2  7738  hartogslem1  7761  cantnflt  7885  cantnfp1lem3  7893  cantnfp1  7894  oemapso  7895  oemapvali  7897  cantnflem1d  7901  cantnflem1  7902  cantnf  7906  oemapwe  7907  cantnffval2  7908  cantnfltOLD  7915  cantnfp1lem3OLD  7919  cantnfp1OLD  7920  cantnflem1dOLD  7924  cantnflem1OLD  7925  cantnfOLD  7928  oemapweOLD  7929  cantnffval2OLD  7930  cnfcom  7938  cnfcomOLD  7946  r111  7987  r1ordg  7990  rankonidlem  8040  bndrank  8053  r1pw  8057  r1pwOLD  8058  rankbnd2  8081  tcrank  8096  cardprclem  8154  carduni  8156  cardmin2  8173  infxpenlem  8185  alephdom  8256  alephdom2  8262  cardaleph  8264  iscard3  8268  alephfp  8283  dfac12lem1  8317  dfac12lem2  8318  dfac12lem3  8319  cflim2  8437  cofsmo  8443  cfsmolem  8444  coftr  8447  cfcof  8448  fin67  8569  hsmexlem5  8604  zorn2lem6  8675  ttukeylem3  8685  ttukeylem5  8687  ttukeylem6  8688  ttukeylem7  8689  winainflem  8865  r1limwun  8908  r1wunlim  8909  tsksuc  8934  inar1  8947  gruina  8990  grur1a  8991  grur1  8992  dfrdg2  27614  poseq  27719  soseq  27720  nodmord  27799  nodenselem5  27831  nofulllem5  27852  ontgval  28282  ontgsucval  28283  onsuctopon  28285  onintopsscon  28291  onsuct0  28292  aomclem4  29415  aomclem5  29416  onfrALTlem3  31257  onfrALTlem2  31259  onfrALTlem3VD  31628  onfrALTlem2VD  31630
  Copyright terms: Public domain W3C validator