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

Theorem eloni 4888
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 4886 . 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 1767   Ord word 4877   Oncon0 4878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-uni 4246  df-tr 4541  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882
This theorem is referenced by:  elon2  4889  onelon  4903  onin  4909  ontri1  4912  onfr  4917  onelpss  4918  onsseleq  4919  onelss  4920  ontr1  4924  ontr2  4925  ordunidif  4926  on0eln0  4933  ordsssuc  4964  onsssuc  4965  onnbtwn  4969  suc11  4981  onordi  4982  onssneli  4987  ordon  6596  ordeleqon  6602  onss  6604  ordsuc  6627  onpwsuc  6629  onpsssuc  6632  onsucmin  6634  ordunpr  6639  ordunisuc  6645  onsucuni2  6647  onuninsuci  6653  ordunisuc2  6657  ordzsl  6658  onzsl  6659  nlimon  6664  tfinds  6672  tfindsg2  6674  nnord  6686  onfununi  7009  smo11  7032  smoord  7033  smoword  7034  smogt  7035  tfrlem1  7042  tfrlem9a  7052  tfrlem15  7058  tz7.44-2  7070  tz7.48lem  7103  oe0m1  7168  oaordi  7192  oaord  7193  oacan  7194  oawordri  7196  oalimcl  7206  oaass  7207  omord2  7213  omcan  7215  omwordi  7217  omword1  7219  omword2  7220  om00  7221  omlimcl  7224  omass  7226  omeulem2  7229  omopth2  7230  oen0  7232  oeord  7234  oecan  7235  oewordi  7237  oeworde  7239  oelimcl  7246  oeeulem  7247  oeeui  7248  nnarcl  7262  nnawordi  7267  nnawordex  7283  oaabs2  7291  omabs  7293  omsmo  7300  omxpenlem  7615  infensuc  7692  onomeneq  7704  ordiso  7937  ordtypelem2  7940  hartogslem1  7963  cantnflt  8087  cantnfp1lem3  8095  cantnfp1  8096  oemapso  8097  oemapvali  8099  cantnflem1d  8103  cantnflem1  8104  cantnf  8108  oemapwe  8109  cantnffval2  8110  cantnfltOLD  8117  cantnfp1lem3OLD  8121  cantnfp1OLD  8122  cantnflem1dOLD  8126  cantnflem1OLD  8127  cantnfOLD  8130  oemapweOLD  8131  cantnffval2OLD  8132  cnfcom  8140  cnfcomOLD  8148  r111  8189  r1ordg  8192  rankonidlem  8242  bndrank  8255  r1pw  8259  r1pwOLD  8260  rankbnd2  8283  tcrank  8298  cardprclem  8356  carduni  8358  cardmin2  8375  infxpenlem  8387  alephdom  8458  alephdom2  8464  cardaleph  8466  iscard3  8470  alephfp  8485  dfac12lem1  8519  dfac12lem2  8520  dfac12lem3  8521  cflim2  8639  cofsmo  8645  cfsmolem  8646  coftr  8649  cfcof  8650  fin67  8771  hsmexlem5  8806  zorn2lem6  8877  ttukeylem3  8887  ttukeylem5  8889  ttukeylem6  8890  ttukeylem7  8891  winainflem  9067  r1limwun  9110  r1wunlim  9111  tsksuc  9136  inar1  9149  gruina  9192  grur1a  9193  grur1  9194  dfrdg2  28805  poseq  28910  soseq  28911  nodmord  28990  nodenselem5  29022  nofulllem5  29043  ontgval  29473  ontgsucval  29474  onsuctopon  29476  onintopsscon  29482  onsuct0  29483  aomclem4  30607  aomclem5  30608  onfrALTlem3  32396  onfrALTlem2  32398  onfrALTlem3VD  32767  onfrALTlem2VD  32769
  Copyright terms: Public domain W3C validator