Theorem ordelon 6356

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 6354	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
2		elong 6340	. . 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 6331  Oncon0 6332

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336

This theorem is referenced by:  onelon  6357  ordunidif  6382  ordpwsuc  7790  ordsucun  7800  ordunel  7802  ordunisuc2  7820  oesuclem  8489  odi  8543  oelim2  8559  oeoalem  8560  oeoelem  8562  limenpsi  9116  ordtypelem9  9479  oismo  9493  cantnflt  9625  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1  9642  rankr1bg  9756  rankr1clem  9773  rankr1c  9774  rankonidlem  9781  infxpenlem  9966  coflim  10214  fin23lem26  10278  fpwwe2lem7  10590  onsuct0  36429  ordnexbtwnsuc  43256  orddif0suc  43257  omord2lim  43289  nadd2rabtr  43373  nadd2rabex  43375  nadd1rabtr  43377  nadd1rabex  43379  iunord  49665