Theorem onelss 6353

Description: An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
onelss	⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Proof of Theorem onelss

Step	Hyp	Ref	Expression
1		eloni 6321	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelss 6327	. . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
3	2	ex 412	. 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	syl 17	1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905  Ord word 6310  Oncon0 6311

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3440  df-ss 3922  df-uni 4862  df-tr 5203  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315

This theorem is referenced by:  ordunidif  6361  onelssi  6427  ssorduni  7719  sucexeloniOLD  7750  tfisi  7799  poseq  8098  tfrlem9  8314  tfrlem11  8317  oaordex  8483  oaass  8486  odi  8504  omass  8505  oewordri  8517  nnaordex  8563  domtriord  9047  hartogs  9455  card2on  9465  tskwe  9865  infxpenlem  9926  cfub  10162  cfsuc  10170  coflim  10174  hsmexlem2  10340  ondomon  10476  pwcfsdom  10496  inar1  10688  tskord  10693  grudomon  10730  gruina  10731  sltres  27590  nosupno  27631  nosupbday  27633  noinfno  27646  oldssmade  27809  madebday  27832  mulsproplem13  28054  mulsproplem14  28055  dfrdg2  35768  aomclem6  43032  nnoeomeqom  43285  naddgeoa  43367  naddwordnexlem1  43370  naddwordnexlem4  43374  iscard5  43509