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

Theorem onordi 4975
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 4881 . 2  |-  ( A  e.  On  ->  Ord  A )
31, 2ax-mp 5 1  |-  Ord  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762   Ord word 4870   Oncon0 4871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-v 3108  df-in 3476  df-ss 3483  df-uni 4239  df-tr 4534  df-po 4793  df-so 4794  df-fr 4831  df-we 4833  df-ord 4874  df-on 4875
This theorem is referenced by:  ontrci  4976  onirri  4977  onun2i  4986  onuniorsuci  6645  onsucssi  6647  oawordeulem  7193  omopthi  7296  bndrank  8248  rankprb  8258  rankuniss  8273  rankelun  8279  rankelpr  8280  rankelop  8281  rankmapu  8285  rankxplim3  8288  rankxpsuc  8289  cardlim  8342  carduni  8351  dfac8b  8401  alephdom2  8457  alephfp  8478  dfac12lem2  8513  pm110.643ALT  8547  cfsmolem  8639  ttukeylem6  8883  ttukeylem7  8884  unsnen  8917  mreexexd  14892  efgmnvl  16521  nodenselem4  29007  hfuni  29404  pwfi2f1o  30637
  Copyright terms: Public domain W3C validator