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

Theorem eloni 4716
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 4714 . 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 1755   Ord word 4705   Oncon0 4706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-v 2964  df-in 3323  df-ss 3330  df-uni 4080  df-tr 4374  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710
This theorem is referenced by:  elon2  4717  onelon  4731  onin  4737  ontri1  4740  onfr  4745  onelpss  4746  onsseleq  4747  onelss  4748  ontr1  4752  ontr2  4753  ordunidif  4754  on0eln0  4761  ordsssuc  4792  onsssuc  4793  onnbtwn  4797  suc11  4809  onordi  4810  onssneli  4815  ordon  6383  ordeleqon  6389  onss  6391  ordsuc  6414  onpwsuc  6416  onpsssuc  6419  onsucmin  6421  ordunpr  6426  ordunisuc  6432  onsucuni2  6434  onuninsuci  6440  ordunisuc2  6444  ordzsl  6445  onzsl  6446  nlimon  6451  tfinds  6459  tfindsg2  6461  nnord  6473  onfununi  6788  smo11  6811  smoord  6812  smoword  6813  smogt  6814  tfrlem1  6821  tfrlem9a  6831  tfrlem15  6837  tz7.44-2  6849  tz7.48lem  6882  oe0m1  6949  oaordi  6973  oaord  6974  oacan  6975  oawordri  6977  oalimcl  6987  oaass  6988  omord2  6994  omcan  6996  omwordi  6998  omword1  7000  omword2  7001  om00  7002  omlimcl  7005  omass  7007  omeulem2  7010  omopth2  7011  oen0  7013  oeord  7015  oecan  7016  oewordi  7018  oeworde  7020  oelimcl  7027  oeeulem  7028  oeeui  7029  nnarcl  7043  nnawordi  7048  nnawordex  7064  oaabs2  7072  omabs  7074  omsmo  7081  omxpenlem  7400  infensuc  7477  onomeneq  7488  ordiso  7718  ordtypelem2  7721  hartogslem1  7744  cantnflt  7868  cantnfp1lem3  7876  cantnfp1  7877  oemapso  7878  oemapvali  7880  cantnflem1d  7884  cantnflem1  7885  cantnf  7889  oemapwe  7890  cantnffval2  7891  cantnfltOLD  7898  cantnfp1lem3OLD  7902  cantnfp1OLD  7903  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnfOLD  7911  oemapweOLD  7912  cantnffval2OLD  7913  cnfcom  7921  cnfcomOLD  7929  r111  7970  r1ordg  7973  rankonidlem  8023  bndrank  8036  r1pw  8040  r1pwOLD  8041  rankbnd2  8064  tcrank  8079  cardprclem  8137  carduni  8139  cardmin2  8156  infxpenlem  8168  alephdom  8239  alephdom2  8245  cardaleph  8247  iscard3  8251  alephfp  8266  dfac12lem1  8300  dfac12lem2  8301  dfac12lem3  8302  cflim2  8420  cofsmo  8426  cfsmolem  8427  coftr  8430  cfcof  8431  fin67  8552  hsmexlem5  8587  zorn2lem6  8658  ttukeylem3  8668  ttukeylem5  8670  ttukeylem6  8671  ttukeylem7  8672  winainflem  8847  r1limwun  8890  r1wunlim  8891  tsksuc  8916  inar1  8929  gruina  8972  grur1a  8973  grur1  8974  dfrdg2  27455  poseq  27560  soseq  27561  nodmord  27640  nodenselem5  27672  nofulllem5  27693  ontgval  28124  ontgsucval  28125  onsuctopon  28127  onintopsscon  28133  onsuct0  28134  aomclem4  29252  aomclem5  29253  onfrALTlem3  30950  onfrALTlem2  30952  onfrALTlem3VD  31322  onfrALTlem2VD  31324
  Copyright terms: Public domain W3C validator