Theorem onelss 6367

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 6335	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelss 6341	. . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
3	2	ex 412	. 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	syl 17	1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  Ord word 6324  Oncon0 6325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3444  df-ss 3920  df-uni 4866  df-tr 5208  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329

This theorem is referenced by:  ordunidif  6375  onelssi  6441  ssorduni  7734  tfisi  7811  poseq  8110  tfrlem9  8326  tfrlem11  8329  oaordex  8495  oaass  8498  odi  8516  omass  8517  oewordri  8530  nnaordex  8576  domtriord  9063  hartogs  9461  card2on  9471  tskwe  9874  infxpenlem  9935  cfub  10171  cfsuc  10179  coflim  10183  hsmexlem2  10349  ondomon  10485  pwcfsdom  10506  inar1  10698  tskord  10703  grudomon  10740  gruina  10741  ltsres  27642  nosupno  27683  nosupbday  27685  noinfno  27698  oldssmade  27875  madebday  27908  mulsproplem13  28136  mulsproplem14  28137  dfrdg2  36006  aomclem6  43405  nnoeomeqom  43658  naddgeoa  43740  naddwordnexlem1  43743  naddwordnexlem4  43747  iscard5  43881