Theorem ordelon 4838

Description: An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.)

Assertion

Ref	Expression
ordelon	|- ( ( Ord A /\ B e. A ) -> B e. On )

Proof of Theorem ordelon

Step	Hyp	Ref	Expression
1		ordelord 4836	. 2 |- ( ( Ord A /\ B e. A ) -> Ord B )
2		elong 4822	. . 3 |- ( B e. A -> ( B e. On <-> Ord B ) )
3	2	adantl 466	. 2 |- ( ( Ord A /\ B e. A ) -> ( B e. On <-> Ord B ) )
4	1, 3	mpbird 232	1 |- ( ( Ord A /\ B e. A ) -> B e. On )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   e. wcel 1758   Ord word 4813   Oncon0 4814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4508  ax-nul 4516  ax-pr 4626

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-ne 2644  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3067  df-dif 3426  df-un 3428  df-in 3430  df-ss 3437  df-nul 3733  df-if 3887  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4187  df-br 4388  df-opab 4446  df-tr 4481  df-eprel 4727  df-po 4736  df-so 4737  df-fr 4774  df-we 4776  df-ord 4817  df-on 4818

This theorem is referenced by:  onelon  4839  ordunidif  4862  ordpwsuc  6523  ordsucun  6533  ordunel  6535  ordunisuc2  6552  oesuclem  7062  odi  7115  oelim2  7131  oeoalem  7132  oeoelem  7134  limenpsi  7583  ordtypelem9  7838  oismo  7852  cantnflt  7978  cantnfp1lem3  7986  cantnflem1b  7992  cantnflem1  7995  cantnfltOLD  8008  cantnfp1lem3OLD  8012  cantnflem1bOLD  8015  cantnflem1OLD  8018  rankr1bg  8108  rankr1clem  8125  rankr1c  8126  rankonidlem  8133  infxpenlem  8278  coflim  8528  fin23lem26  8592  fpwwe2lem8  8902  nofulllem5  27978  onsuct0  28418