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

Theorem onordi 5830
 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 5731 . 2 (𝐴 ∈ On → Ord 𝐴)
31, 2ax-mp 5 1 Ord 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 1989  Ord word 5720  Oncon0 5721 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-rex 2917  df-v 3200  df-in 3579  df-ss 3586  df-uni 4435  df-tr 4751  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-ord 5724  df-on 5725 This theorem is referenced by:  ontrci  5831  onirri  5832  onun2i  5841  onuniorsuci  7036  onsucssi  7038  oawordeulem  7631  omopthi  7734  bndrank  8701  rankprb  8711  rankuniss  8726  rankelun  8732  rankelpr  8733  rankelop  8734  rankmapu  8738  rankxplim3  8741  rankxpsuc  8742  cardlim  8795  carduni  8804  dfac8b  8851  alephdom2  8907  alephfp  8928  dfac12lem2  8963  pm110.643ALT  8997  cfsmolem  9089  ttukeylem6  9333  ttukeylem7  9334  unsnen  9372  mreexexdOLD  16303  efgmnvl  18121  slerec  31907  hfuni  32275  finxpsuclem  33214  pwfi2f1o  37492
 Copyright terms: Public domain W3C validator