Theorem onelss 6394

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926  Ord word 6351  Oncon0 6352

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-ss 3943  df-uni 4884  df-tr 5230  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356

This theorem is referenced by:  ordunidif  6402  onelssi  6469  ssorduni  7773  sucexeloniOLD  7804  suceloniOLD  7806  tfisi  7854  poseq  8157  tfrlem9  8399  tfrlem11  8402  oaordex  8570  oaass  8573  odi  8591  omass  8592  oewordri  8604  nnaordex  8650  domtriord  9137  hartogs  9558  card2on  9568  tskwe  9964  infxpenlem  10027  cfub  10263  cfsuc  10271  coflim  10275  hsmexlem2  10441  ondomon  10577  pwcfsdom  10597  inar1  10789  tskord  10794  grudomon  10831  gruina  10832  sltres  27626  nosupno  27667  nosupbday  27669  noinfno  27682  oldssmade  27841  madebday  27863  mulsproplem13  28083  mulsproplem14  28084  dfrdg2  35813  aomclem6  43083  nnoeomeqom  43336  naddgeoa  43418  naddwordnexlem1  43421  naddwordnexlem4  43425  iscard5  43560