Theorem onelss 6357

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  Ord word 6314  Oncon0 6315

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 3432  df-ss 3907  df-uni 4852  df-tr 5194  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319

This theorem is referenced by:  ordunidif  6365  onelssi  6431  ssorduni  7724  tfisi  7801  poseq  8099  tfrlem9  8315  tfrlem11  8318  oaordex  8484  oaass  8487  odi  8505  omass  8506  oewordri  8519  nnaordex  8565  domtriord  9052  hartogs  9450  card2on  9460  tskwe  9863  infxpenlem  9924  cfub  10160  cfsuc  10168  coflim  10172  hsmexlem2  10338  ondomon  10474  pwcfsdom  10495  inar1  10687  tskord  10692  grudomon  10729  gruina  10730  ltsres  27645  nosupno  27686  nosupbday  27688  noinfno  27701  oldssmade  27878  madebday  27911  mulsproplem13  28139  mulsproplem14  28140  dfrdg2  35996  aomclem6  43502  nnoeomeqom  43755  naddgeoa  43837  naddwordnexlem1  43840  naddwordnexlem4  43844  iscard5  43978