MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eloni Structured 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 244 1  |-  ( A  e.  On  ->  Ord  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   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 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-v 3089  df-in 3449  df-ss 3456  df-uni 4223  df-tr 4521  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  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  6623  ordeleqon  6629  onss  6631  ordsuc  6655  onpwsuc  6657  onpsssuc  6660  onsucmin  6662  ordunpr  6667  ordunisuc  6673  onsucuni2  6675  onuninsuci  6681  ordunisuc2  6685  ordzsl  6686  onzsl  6687  nlimon  6692  tfinds  6700  tfindsg2  6702  nnord  6714  onfununi  7068  smo11  7091  smoord  7092  smoword  7093  smogt  7094  tfrlem1  7102  tfrlem9a  7112  tfrlem15  7118  tz7.44-2  7133  tz7.48lem  7166  oe0m1  7231  oaordi  7255  oaord  7256  oacan  7257  oawordri  7259  oalimcl  7269  oaass  7270  omord2  7276  omcan  7278  omwordi  7280  omword1  7282  omword2  7283  om00  7284  omlimcl  7287  omass  7289  omeulem2  7292  omopth2  7293  oen0  7295  oeord  7297  oecan  7298  oewordi  7300  oeworde  7302  oelimcl  7309  oeeulem  7310  oeeui  7311  nnarcl  7325  nnawordi  7330  nnawordex  7346  oaabs2  7354  omabs  7356  omsmo  7363  omxpenlem  7679  infensuc  7756  onomeneq  7768  ordiso  8031  ordtypelem2  8034  hartogslem1  8057  cantnflt  8176  cantnfp1lem3  8184  cantnfp1  8185  oemapso  8186  oemapvali  8188  cantnflem1d  8192  cantnflem1  8193  cantnf  8197  oemapwe  8198  cantnffval2  8199  cnfcom  8204  r111  8245  r1ordg  8248  rankonidlem  8298  bndrank  8311  r1pw  8315  r1pwALT  8316  rankbnd2  8339  tcrank  8354  cardprclem  8412  carduni  8414  cardmin2  8431  infxpenlem  8443  alephdom  8510  alephdom2  8516  cardaleph  8518  iscard3  8522  alephfp  8537  dfac12lem1  8571  dfac12lem2  8572  dfac12lem3  8573  cflim2  8691  cofsmo  8697  cfsmolem  8698  coftr  8701  cfcof  8702  fin67  8823  hsmexlem5  8858  zorn2lem6  8929  ttukeylem3  8939  ttukeylem5  8941  ttukeylem6  8942  ttukeylem7  8943  winainflem  9117  r1limwun  9160  r1wunlim  9161  tsksuc  9186  inar1  9199  gruina  9242  grur1a  9243  grur1  9244  dfrdg2  30229  poseq  30278  soseq  30279  nodmord  30327  nodenselem5  30359  nofulllem5  30380  ontgval  30876  ontgsucval  30877  onsuctopon  30879  onintopsscon  30885  onsuct0  30886  aomclem4  35621  aomclem5  35622  onfrALTlem3  36547  onfrALTlem2  36549  onfrALTlem3VD  36924  onfrALTlem2VD  36926
  Copyright terms: Public domain W3C validator