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

Theorem eloni 4404
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 4402 . 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 1686   Ord word 4393   Oncon0 4394
This theorem is referenced by:  elon2  4405  onelon  4419  onin  4425  ontri1  4428  onfr  4433  onelpss  4434  onsseleq  4435  onelss  4436  ontr1  4440  ontr2  4441  ordunidif  4442  on0eln0  4449  ordsssuc  4481  onsssuc  4482  onnbtwn  4486  suc11  4498  onordi  4499  onssneli  4504  ordon  4576  ordeleqon  4582  onss  4584  ordsuc  4607  onpwsuc  4609  onpsssuc  4612  onsucmin  4614  ordunpr  4619  ordunisuc  4625  onsucuni2  4627  onuninsuci  4633  ordunisuc2  4637  ordzsl  4638  onzsl  4639  nlimon  4644  tfinds  4652  tfindsg2  4654  nnord  4666  onfununi  6360  smo11  6383  smoord  6384  smoword  6385  smogt  6386  tfrlem9a  6404  tfrlem15  6410  tz7.44-2  6422  tz7.48lem  6455  oe0m1  6522  oaordi  6546  oaord  6547  oacan  6548  oawordri  6550  oalimcl  6560  oaass  6561  omord2  6567  omcan  6569  omwordi  6571  omword1  6573  omword2  6574  om00  6575  omlimcl  6578  omass  6580  omeulem2  6583  omopth2  6584  oen0  6586  oeord  6588  oecan  6589  oewordi  6591  oeworde  6593  oelimcl  6600  oeeulem  6601  oeeui  6602  nnarcl  6616  nnawordi  6621  nnawordex  6637  oaabs2  6645  omabs  6647  omsmo  6654  omxpenlem  6965  infensuc  7041  onomeneq  7052  ordiso  7233  ordtypelem2  7236  hartogslem1  7259  cantnflt  7375  cantnfp1lem3  7384  cantnfp1  7385  oemapso  7386  oemapvali  7388  cantnflem1d  7392  cantnflem1  7393  cantnf  7397  oemapwe  7398  cantnffval2  7399  cnfcom  7405  r111  7449  r1ordg  7452  rankonidlem  7502  bndrank  7515  r1pw  7519  r1pwOLD  7520  rankbnd2  7543  tcrank  7556  cardprclem  7614  carduni  7616  cardmin2  7633  infxpenlem  7643  alephdom  7710  alephdom2  7716  cardaleph  7718  iscard3  7722  alephfp  7737  dfac12lem1  7771  dfac12lem2  7772  dfac12lem3  7773  cflim2  7891  cofsmo  7897  cfsmolem  7898  coftr  7901  cfcof  7902  fin67  8023  hsmexlem5  8058  zorn2lem6  8130  ttukeylem3  8140  ttukeylem5  8142  ttukeylem6  8143  ttukeylem7  8144  winainflem  8317  r1limwun  8360  r1wunlim  8361  tsksuc  8386  inar1  8399  gruina  8442  grur1a  8443  grur1  8444  dfrdg2  24154  poseq  24255  soseq  24256  nodmord  24309  nodenselem5  24341  nofulllem5  24362  ontgval  24872  ontgsucval  24873  onsuctopon  24875  onintopsscon  24881  onsuct0  24882  ordsuccl2  25114  ordsuccl3  25115  celsor  25122  vtarl  25898  tartarmap  25899  eltintpar  25910  inttaror  25911  aomclem4  27165  aomclem5  27166  onfrALTlem3  28365  onfrALTlem2  28367  onfrALTlem3VD  28736  onfrALTlem2VD  28738
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550  df-rex 2551  df-v 2792  df-in 3161  df-ss 3168  df-uni 3830  df-tr 4116  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398
  Copyright terms: Public domain W3C validator