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

Theorem eloni 4418
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 4416 . 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 1696   Ord word 4407   Oncon0 4408
This theorem is referenced by:  elon2  4419  onelon  4433  onin  4439  ontri1  4442  onfr  4447  onelpss  4448  onsseleq  4449  onelss  4450  ontr1  4454  ontr2  4455  ordunidif  4456  on0eln0  4463  ordsssuc  4495  onsssuc  4496  onnbtwn  4500  suc11  4512  onordi  4513  onssneli  4518  ordon  4590  ordeleqon  4596  onss  4598  ordsuc  4621  onpwsuc  4623  onpsssuc  4626  onsucmin  4628  ordunpr  4633  ordunisuc  4639  onsucuni2  4641  onuninsuci  4647  ordunisuc2  4651  ordzsl  4652  onzsl  4653  nlimon  4658  tfinds  4666  tfindsg2  4668  nnord  4680  onfununi  6374  smo11  6397  smoord  6398  smoword  6399  smogt  6400  tfrlem9a  6418  tfrlem15  6424  tz7.44-2  6436  tz7.48lem  6469  oe0m1  6536  oaordi  6560  oaord  6561  oacan  6562  oawordri  6564  oalimcl  6574  oaass  6575  omord2  6581  omcan  6583  omwordi  6585  omword1  6587  omword2  6588  om00  6589  omlimcl  6592  omass  6594  omeulem2  6597  omopth2  6598  oen0  6600  oeord  6602  oecan  6603  oewordi  6605  oeworde  6607  oelimcl  6614  oeeulem  6615  oeeui  6616  nnarcl  6630  nnawordi  6635  nnawordex  6651  oaabs2  6659  omabs  6661  omsmo  6668  omxpenlem  6979  infensuc  7055  onomeneq  7066  ordiso  7247  ordtypelem2  7250  hartogslem1  7273  cantnflt  7389  cantnfp1lem3  7398  cantnfp1  7399  oemapso  7400  oemapvali  7402  cantnflem1d  7406  cantnflem1  7407  cantnf  7411  oemapwe  7412  cantnffval2  7413  cnfcom  7419  r111  7463  r1ordg  7466  rankonidlem  7516  bndrank  7529  r1pw  7533  r1pwOLD  7534  rankbnd2  7557  tcrank  7570  cardprclem  7628  carduni  7630  cardmin2  7647  infxpenlem  7657  alephdom  7724  alephdom2  7730  cardaleph  7732  iscard3  7736  alephfp  7751  dfac12lem1  7785  dfac12lem2  7786  dfac12lem3  7787  cflim2  7905  cofsmo  7911  cfsmolem  7912  coftr  7915  cfcof  7916  fin67  8037  hsmexlem5  8072  zorn2lem6  8144  ttukeylem3  8154  ttukeylem5  8156  ttukeylem6  8157  ttukeylem7  8158  winainflem  8331  r1limwun  8374  r1wunlim  8375  tsksuc  8400  inar1  8413  gruina  8456  grur1a  8457  grur1  8458  dfrdg2  24223  poseq  24324  soseq  24325  nodmord  24378  nodenselem5  24410  nofulllem5  24431  ontgval  24942  ontgsucval  24943  onsuctopon  24945  onintopsscon  24951  onsuct0  24952  ordsuccl2  25206  ordsuccl3  25207  celsor  25214  vtarl  25990  tartarmap  25991  eltintpar  26002  inttaror  26003  aomclem4  27257  aomclem5  27258  onfrALTlem3  28608  onfrALTlem2  28610  onfrALTlem3VD  28979  onfrALTlem2VD  28981
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-v 2803  df-in 3172  df-ss 3179  df-uni 3844  df-tr 4130  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412
  Copyright terms: Public domain W3C validator