Theorem ordelon 6359

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 6357	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
2		elong 6343	. . 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 2109  Ord word 6334  Oncon0 6335

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339

This theorem is referenced by:  onelon  6360  ordunidif  6385  ordpwsuc  7793  ordsucun  7803  ordunel  7805  ordunisuc2  7823  oesuclem  8492  odi  8546  oelim2  8562  oeoalem  8563  oeoelem  8565  limenpsi  9122  ordtypelem9  9486  oismo  9500  cantnflt  9632  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1  9649  rankr1bg  9763  rankr1clem  9780  rankr1c  9781  rankonidlem  9788  infxpenlem  9973  coflim  10221  fin23lem26  10285  fpwwe2lem7  10597  onsuct0  36436  ordnexbtwnsuc  43263  orddif0suc  43264  omord2lim  43296  nadd2rabtr  43380  nadd2rabex  43382  nadd1rabtr  43384  nadd1rabex  43386  iunord  49669