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

Theorem onordi 4626
Description: An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
on.1  |-  A  e.  On
Assertion
Ref Expression
onordi  |-  Ord  A

Proof of Theorem onordi
StepHypRef Expression
1 on.1 . 2  |-  A  e.  On
2 eloni 4532 . 2  |-  ( A  e.  On  ->  Ord  A )
31, 2ax-mp 8 1  |-  Ord  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   Ord word 4521   Oncon0 4522
This theorem is referenced by:  ontrci  4627  onirri  4628  onun2i  4637  onuniorsuci  4759  onsucssi  4761  oawordeulem  6733  omopthi  6836  bndrank  7700  rankprb  7710  rankuniss  7725  rankelun  7731  rankelpr  7732  rankelop  7733  rankxplim3  7738  rankxpsuc  7739  cardlim  7792  carduni  7801  dfac8b  7845  alephdom2  7901  alephfp  7922  dfac12lem2  7957  pm110.643ALT  7991  cfsmolem  8083  ttukeylem6  8327  ttukeylem7  8328  unsnen  8361  mreexexd  13800  efgmnvl  15273  nodenselem4  25362  hfuni  25839  pwfi2f1o  26929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-rex 2655  df-v 2901  df-in 3270  df-ss 3277  df-uni 3958  df-tr 4244  df-po 4444  df-so 4445  df-fr 4482  df-we 4484  df-ord 4525  df-on 4526
  Copyright terms: Public domain W3C validator