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

Theorem eloni 5452
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 5450 . 2  |-  ( A  e.  On  ->  ( A  e.  On  <->  Ord  A ) )
21ibi 249 1  |-  ( A  e.  On  ->  Ord  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   Ord word 5441   Oncon0 5442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-v 3059  df-in 3423  df-ss 3430  df-uni 4213  df-tr 4512  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-ord 5445  df-on 5446
This theorem is referenced by:  elon2  5453  onelon  5467  onin  5473  ontri1  5476  onfr  5481  onelpss  5482  onsseleq  5483  onelss  5484  ontr1  5488  ontr2  5489  ordunidif  5490  on0eln0  5497  ordsssuc  5528  onsssuc  5529  onnbtwn  5533  suc11  5545  onordi  5546  onssneli  5551  ordon  6636  ordeleqon  6642  onss  6644  ordsuc  6668  onpwsuc  6670  onpsssuc  6673  onsucmin  6675  ordunpr  6680  ordunisuc  6686  onsucuni2  6688  onuninsuci  6694  ordunisuc2  6698  ordzsl  6699  onzsl  6700  nlimon  6705  tfinds  6713  tfindsg2  6715  nnord  6727  onfununi  7086  smo11  7109  smoord  7110  smoword  7111  smogt  7112  tfrlem1  7120  tfrlem9a  7130  tfrlem15  7136  tz7.44-2  7151  tz7.48lem  7184  oe0m1  7249  oaordi  7273  oaord  7274  oacan  7275  oawordri  7277  oalimcl  7287  oaass  7288  omord2  7294  omcan  7296  omwordi  7298  omword1  7300  omword2  7301  om00  7302  omlimcl  7305  omass  7307  omeulem2  7310  omopth2  7311  oen0  7313  oeord  7315  oecan  7316  oewordi  7318  oeworde  7320  oelimcl  7327  oeeulem  7328  oeeui  7329  nnarcl  7343  nnawordi  7348  nnawordex  7364  oaabs2  7372  omabs  7374  omsmo  7381  omxpenlem  7699  infensuc  7776  onomeneq  7788  ordiso  8057  ordtypelem2  8060  hartogslem1  8083  cantnflt  8203  cantnfp1lem3  8211  cantnfp1  8212  oemapso  8213  oemapvali  8215  cantnflem1d  8219  cantnflem1  8220  cantnf  8224  oemapwe  8225  cantnffval2  8226  cnfcom  8231  r111  8272  r1ordg  8275  rankonidlem  8325  bndrank  8338  r1pw  8342  r1pwALT  8343  rankbnd2  8366  tcrank  8381  cardprclem  8439  carduni  8441  cardmin2  8458  infxpenlem  8470  alephdom  8538  alephdom2  8544  cardaleph  8546  iscard3  8550  alephfp  8565  dfac12lem1  8599  dfac12lem2  8600  dfac12lem3  8601  cflim2  8719  cofsmo  8725  cfsmolem  8726  coftr  8729  cfcof  8730  fin67  8851  hsmexlem5  8886  zorn2lem6  8957  ttukeylem3  8967  ttukeylem5  8969  ttukeylem6  8970  ttukeylem7  8971  winainflem  9144  r1limwun  9187  r1wunlim  9188  tsksuc  9213  inar1  9226  gruina  9269  grur1a  9270  grur1  9271  dfrdg2  30491  poseq  30540  soseq  30541  nodmord  30589  nodenselem5  30623  nofulllem5  30644  ontgval  31140  ontgsucval  31141  onsuctopon  31143  onintopsscon  31149  onsuct0  31150  sucneqond  31813  onsucuni3  31815  aomclem4  35960  aomclem5  35961  onfrALTlem3  36954  onfrALTlem2  36956  onfrALTlem3VD  37324  onfrALTlem2VD  37326
  Copyright terms: Public domain W3C validator