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

Theorem onordi 4821
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 4727 . 2  |-  ( A  e.  On  ->  Ord  A )
31, 2ax-mp 5 1  |-  Ord  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   Ord word 4716   Oncon0 4717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-v 2972  df-in 3333  df-ss 3340  df-uni 4090  df-tr 4384  df-po 4639  df-so 4640  df-fr 4677  df-we 4679  df-ord 4720  df-on 4721
This theorem is referenced by:  ontrci  4822  onirri  4823  onun2i  4832  onuniorsuci  6448  onsucssi  6450  oawordeulem  6991  omopthi  7094  bndrank  8046  rankprb  8056  rankuniss  8071  rankelun  8077  rankelpr  8078  rankelop  8079  rankmapu  8083  rankxplim3  8086  rankxpsuc  8087  cardlim  8140  carduni  8149  dfac8b  8199  alephdom2  8255  alephfp  8276  dfac12lem2  8311  pm110.643ALT  8345  cfsmolem  8437  ttukeylem6  8681  ttukeylem7  8682  unsnen  8715  mreexexd  14584  efgmnvl  16209  nodenselem4  27823  hfuni  28220  pwfi2f1o  29448
  Copyright terms: Public domain W3C validator