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

Step	Hyp	Ref	Expression
1		on.1	. 2 ⊢ 𝐴 ∈ On
2		eloni 6370	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	ax-mp 5	1 ⊢ Ord 𝐴

Syntax hints:   ∈ wcel 2143  Ord word 6359  Oncon0 6360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-ss 3922  df-uni 4873  df-tr 5219  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364

This theorem is referenced by:  onirri  6475  onsucssi  7833  ord1eln01  8477  ord2eln012  8478  oawordeulem  8535  omopthi  8643  en2  9236  en3  9237  ssttrcl  9680  ttrcltr  9681  dmttrcl  9686  ttrclselem2  9691  bndrank  9809  rankprb  9819  rankuniss  9834  rankelun  9840  rankelpr  9841  rankelop  9842  rankmapu  9846  rankxplim3  9849  rankxpsuc  9850  cardlim  9954  carduni  9963  dfac8b  10011  alephdom2  10067  alephfp  10088  dfac12lem2  10124  dju1p1e2ALT  10154  cfsmolem  10249  ttukeylem6  10493  ttukeylem7  10494  unsnen  10532  efgmnvl  19779  nogt01o  27860  cutbdaybnd2lim  27990  lesrec  27992  bday1  28007  cuteq1  28010  newbday  28095  negsproplem7  28227  mulsproplem13  28321  mulsproplem14  28322  ltonold  28454  addonbday  28472  bdaypw2n0bndlem  28656  z12bdaylem  28677  rankscottu  35523  hfuni  36676  finxpsuclem  38043  pwfi2f1o  43823  nelsubc3  49849