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

Theorem eloni 4877
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 4875 . 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 1823   Ord word 4866   Oncon0 4867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-v 3108  df-in 3468  df-ss 3475  df-uni 4236  df-tr 4533  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871
This theorem is referenced by:  elon2  4878  onelon  4892  onin  4898  ontri1  4901  onfr  4906  onelpss  4907  onsseleq  4908  onelss  4909  ontr1  4913  ontr2  4914  ordunidif  4915  on0eln0  4922  ordsssuc  4953  onsssuc  4954  onnbtwn  4958  suc11  4970  onordi  4971  onssneli  4976  ordon  6591  ordeleqon  6597  onss  6599  ordsuc  6622  onpwsuc  6624  onpsssuc  6627  onsucmin  6629  ordunpr  6634  ordunisuc  6640  onsucuni2  6642  onuninsuci  6648  ordunisuc2  6652  ordzsl  6653  onzsl  6654  nlimon  6659  tfinds  6667  tfindsg2  6669  nnord  6681  onfununi  7004  smo11  7027  smoord  7028  smoword  7029  smogt  7030  tfrlem1  7037  tfrlem9a  7047  tfrlem15  7053  tz7.44-2  7065  tz7.48lem  7098  oe0m1  7163  oaordi  7187  oaord  7188  oacan  7189  oawordri  7191  oalimcl  7201  oaass  7202  omord2  7208  omcan  7210  omwordi  7212  omword1  7214  omword2  7215  om00  7216  omlimcl  7219  omass  7221  omeulem2  7224  omopth2  7225  oen0  7227  oeord  7229  oecan  7230  oewordi  7232  oeworde  7234  oelimcl  7241  oeeulem  7242  oeeui  7243  nnarcl  7257  nnawordi  7262  nnawordex  7278  oaabs2  7286  omabs  7288  omsmo  7295  omxpenlem  7611  infensuc  7688  onomeneq  7700  ordiso  7933  ordtypelem2  7936  hartogslem1  7959  cantnflt  8082  cantnfp1lem3  8090  cantnfp1  8091  oemapso  8092  oemapvali  8094  cantnflem1d  8098  cantnflem1  8099  cantnf  8103  oemapwe  8104  cantnffval2  8105  cantnfltOLD  8112  cantnfp1lem3OLD  8116  cantnfp1OLD  8117  cantnflem1dOLD  8121  cantnflem1OLD  8122  cantnfOLD  8125  oemapweOLD  8126  cantnffval2OLD  8127  cnfcom  8135  cnfcomOLD  8143  r111  8184  r1ordg  8187  rankonidlem  8237  bndrank  8250  r1pw  8254  r1pwALT  8255  rankbnd2  8278  tcrank  8293  cardprclem  8351  carduni  8353  cardmin2  8370  infxpenlem  8382  alephdom  8453  alephdom2  8459  cardaleph  8461  iscard3  8465  alephfp  8480  dfac12lem1  8514  dfac12lem2  8515  dfac12lem3  8516  cflim2  8634  cofsmo  8640  cfsmolem  8641  coftr  8644  cfcof  8645  fin67  8766  hsmexlem5  8801  zorn2lem6  8872  ttukeylem3  8882  ttukeylem5  8884  ttukeylem6  8885  ttukeylem7  8886  winainflem  9060  r1limwun  9103  r1wunlim  9104  tsksuc  9129  inar1  9142  gruina  9185  grur1a  9186  grur1  9187  dfrdg2  29468  poseq  29573  soseq  29574  nodmord  29653  nodenselem5  29685  nofulllem5  29706  ontgval  30124  ontgsucval  30125  onsuctopon  30127  onintopsscon  30133  onsuct0  30134  aomclem4  31242  aomclem5  31243  onfrALTlem3  33710  onfrALTlem2  33712  onfrALTlem3VD  34088  onfrALTlem2VD  34090
  Copyright terms: Public domain W3C validator