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

Theorem eloni 4402
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 4400 . 2  |-  ( A  e.  On  ->  ( A  e.  On  <->  Ord  A ) )
21ibi 232 1  |-  ( A  e.  On  ->  Ord  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   Ord word 4391   Oncon0 4392
This theorem is referenced by:  elon2  4403  onelon  4417  onin  4423  ontri1  4426  onfr  4431  onelpss  4432  onsseleq  4433  onelss  4434  ontr1  4438  ontr2  4439  ordunidif  4440  on0eln0  4447  ordsssuc  4479  onsssuc  4480  onnbtwn  4484  suc11  4496  onordi  4497  onssneli  4502  ordon  4574  ordeleqon  4580  onss  4582  ordsuc  4605  onpwsuc  4607  onpsssuc  4610  onsucmin  4612  ordunpr  4617  ordunisuc  4623  onsucuni2  4625  onuninsuci  4631  ordunisuc2  4635  ordzsl  4636  onzsl  4637  nlimon  4642  tfinds  4650  tfindsg2  4652  nnord  4664  onfununi  6358  smo11  6381  smoord  6382  smoword  6383  smogt  6384  tfrlem9a  6402  tfrlem15  6408  tz7.44-2  6420  tz7.48lem  6453  oe0m1  6520  oaordi  6544  oaord  6545  oacan  6546  oawordri  6548  oalimcl  6558  oaass  6559  omord2  6565  omcan  6567  omwordi  6569  omword1  6571  omword2  6572  om00  6573  omlimcl  6576  omass  6578  omeulem2  6581  omopth2  6582  oen0  6584  oeord  6586  oecan  6587  oewordi  6589  oeworde  6591  oelimcl  6598  oeeulem  6599  oeeui  6600  nnarcl  6614  nnawordi  6619  nnawordex  6635  oaabs2  6643  omabs  6645  omsmo  6652  omxpenlem  6963  infensuc  7039  onomeneq  7050  ordiso  7231  ordtypelem2  7234  hartogslem1  7257  cantnflt  7373  cantnfp1lem3  7382  cantnfp1  7383  oemapso  7384  oemapvali  7386  cantnflem1d  7390  cantnflem1  7391  cantnf  7395  oemapwe  7396  cantnffval2  7397  cnfcom  7403  r111  7447  r1ordg  7450  rankonidlem  7500  bndrank  7513  r1pw  7517  r1pwOLD  7518  rankbnd2  7541  tcrank  7554  cardprclem  7612  carduni  7614  cardmin2  7631  infxpenlem  7641  alephdom  7708  alephdom2  7714  cardaleph  7716  iscard3  7720  alephfp  7735  dfac12lem1  7769  dfac12lem2  7770  dfac12lem3  7771  cflim2  7889  cofsmo  7895  cfsmolem  7896  coftr  7899  cfcof  7900  fin67  8021  hsmexlem5  8056  zorn2lem6  8128  ttukeylem3  8138  ttukeylem5  8140  ttukeylem6  8141  ttukeylem7  8142  winainflem  8315  r1limwun  8358  r1wunlim  8359  tsksuc  8384  inar1  8397  gruina  8440  grur1a  8441  grur1  8442  dfrdg2  24152  poseq  24253  soseq  24254  nodmord  24307  nodenselem5  24339  nofulllem5  24360  ontgval  24870  ontgsucval  24871  onsuctopon  24873  onintopsscon  24879  onsuct0  24880  ordsuccl2  25103  ordsuccl3  25104  celsor  25111  vtarl  25887  tartarmap  25888  eltintpar  25899  inttaror  25900  aomclem4  27154  aomclem5  27155  onfrALTlem3  28309  onfrALTlem2  28311  onfrALTlem3VD  28663  onfrALTlem2VD  28665
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-in 3159  df-ss 3166  df-uni 3828  df-tr 4114  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396
  Copyright terms: Public domain W3C validator