Theorem ordelon 6408

Description: An element of an ordinal class is an ordinal number. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.)

Assertion

Ref	Expression
ordelon	⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Proof of Theorem ordelon

Step	Hyp	Ref	Expression
1		ordelord 6406	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
2		elong 6392	. . 3 ⊢ (𝐵 ∈ 𝐴 → (𝐵 ∈ On ↔ Ord 𝐵))
3	2	adantl 481	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ∈ On ↔ Ord 𝐵))
4	1, 3	mpbird 257	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  Ord word 6383  Oncon0 6384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388

This theorem is referenced by:  onelon  6409  ordunidif  6433  ordpwsuc  7835  ordsucun  7845  ordunel  7847  ordunisuc2  7865  oesuclem  8563  odi  8617  oelim2  8633  oeoalem  8634  oeoelem  8636  limenpsi  9192  ordtypelem9  9566  oismo  9580  cantnflt  9712  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  rankr1bg  9843  rankr1clem  9860  rankr1c  9861  rankonidlem  9868  infxpenlem  10053  coflim  10301  fin23lem26  10365  fpwwe2lem7  10677  onsuct0  36442  ordnexbtwnsuc  43280  orddif0suc  43281  omord2lim  43313  nadd2rabtr  43397  nadd2rabex  43399  nadd1rabtr  43401  nadd1rabex  43403  iunord  49195