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

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

Proof of Theorem onordi
StepHypRef Expression
1 on.1 . 2 𝐴 ∈ On
2 eloni 5650 . 2 (𝐴 ∈ On → Ord 𝐴)
31, 2ax-mp 5 1 Ord 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  Ord word 5639  Oncon0 5640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373  df-tr 4681  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644
This theorem is referenced by:  ontrci  5750  onirri  5751  onun2i  5760  onuniorsuci  6931  onsucssi  6933  oawordeulem  7521  omopthi  7624  bndrank  8587  rankprb  8597  rankuniss  8612  rankelun  8618  rankelpr  8619  rankelop  8620  rankmapu  8624  rankxplim3  8627  rankxpsuc  8628  cardlim  8681  carduni  8690  dfac8b  8737  alephdom2  8793  alephfp  8814  dfac12lem2  8849  pm110.643ALT  8883  cfsmolem  8975  ttukeylem6  9219  ttukeylem7  9220  unsnen  9254  mreexexdOLD  16132  efgmnvl  17950  nodenselem4  31083  hfuni  31461  finxpsuclem  32410  pwfi2f1o  36684
  Copyright terms: Public domain W3C validator