Theorem onordi 6502

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 6398	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	ax-mp 5	1 ⊢ Ord 𝐴

This proof depends on syntax axioms:   ∈ wcel 2147  Ord word 6387  Oncon0 6388

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-ss 3901  df-uni 4873  df-tr 5219  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392

This theorem is used by:  onirri  6503  onsucssi  7886  ord1eln01  8542  ord2eln012  8543  oawordeulem  8600  omopthi  8708  en2  9309  en3  9310  ssttrcl  9753  ttrcltr  9754  dmttrcl  9759  ttrclselem2  9764  bndrank  9891  rankprb  9902  rankuniss  9920  rankelun  9926  rankelpr  9927  rankelop  9928  rankmapu  9932  rankxplim3  9935  rankxpsuc  9936  hfuniOLD  9962  cardlim  10090  carduni  10101  dfac8b  10149  alephdom2  10205  alephfp  10226  dfac12lem2  10262  dju1p1e2ALT  10292  cfsmolem  10387  ttukeylem6  10631  ttukeylem7  10632  unsnen  10676  efgmnvl  19979  nogt01o  28110  cutbdaybnd2lim  28240  lesrec  28242  bday1  28257  cuteq1  28260  newbday  28345  negsproplem7  28477  mulsproplem13  28571  mulsproplem14  28572  ltonold  28704  addonbday  28722  bdaypw2n0bndlem  28906  z12bdaylem  28927  rankscottu  35880  finxpsuclem  38588  findcard4  38900  pwfi2f1o  44364  nelsubc3  50516