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

Theorem onordi 6267
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 6173 . 2 (𝐴 ∈ On → Ord 𝐴)
31, 2ax-mp 5 1 Ord 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  Ord word 6162  Oncon0 6163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-v 3446  df-in 3891  df-ss 3901  df-uni 4804  df-tr 5140  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-ord 6166  df-on 6167
This theorem is referenced by:  ontrci  6268  onirri  6269  onun2i  6278  onuniorsuci  7538  onsucssi  7540  oawordeulem  8167  omopthi  8271  bndrank  9258  rankprb  9268  rankuniss  9283  rankelun  9289  rankelpr  9290  rankelop  9291  rankmapu  9295  rankxplim3  9298  rankxpsuc  9299  cardlim  9389  carduni  9398  dfac8b  9446  alephdom2  9502  alephfp  9523  dfac12lem2  9559  dju1p1e2ALT  9589  cfsmolem  9685  ttukeylem6  9929  ttukeylem7  9930  unsnen  9968  efgmnvl  18836  slerec  33391  hfuni  33759  finxpsuclem  34815  pwfi2f1o  40033
  Copyright terms: Public domain W3C validator