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

Theorem onordi 6474
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 6373 . 2 (𝐴 ∈ On → Ord 𝐴)
31, 2ax-mp 5 1 Ord 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2099  Ord word 6362  Oncon0 6363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-v 3471  df-in 3951  df-ss 3961  df-uni 4904  df-tr 5260  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-ord 6366  df-on 6367
This theorem is referenced by:  onirri  6476  onsucssi  7839  ord1eln01  8510  ord2eln012  8511  oawordeulem  8568  omopthi  8675  en2  9297  en3  9298  ssttrcl  9730  ttrcltr  9731  dmttrcl  9736  ttrclselem2  9741  bndrank  9856  rankprb  9866  rankuniss  9881  rankelun  9887  rankelpr  9888  rankelop  9889  rankmapu  9893  rankxplim3  9896  rankxpsuc  9897  cardlim  9987  carduni  9996  dfac8b  10046  alephdom2  10102  alephfp  10123  dfac12lem2  10159  dju1p1e2ALT  10189  cfsmolem  10285  ttukeylem6  10529  ttukeylem7  10530  unsnen  10568  efgmnvl  19660  nogt01o  27616  scutbdaybnd2lim  27737  slerec  27739  bday1s  27751  cuteq1  27753  newbday  27815  negsproplem7  27933  mulsproplem13  28015  mulsproplem14  28016  sltonold  28140  hfuni  35716  finxpsuclem  36812  pwfi2f1o  42442
  Copyright terms: Public domain W3C validator