Theorem onelss 6344

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3900  Ord word 6301  Oncon0 6302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3436  df-ss 3917  df-uni 4858  df-tr 5197  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6305  df-on 6306

This theorem is referenced by:  ordunidif  6352  onelssi  6418  ssorduni  7707  tfisi  7784  poseq  8083  tfrlem9  8299  tfrlem11  8302  oaordex  8468  oaass  8471  odi  8489  omass  8490  oewordri  8502  nnaordex  8548  domtriord  9031  hartogs  9425  card2on  9435  tskwe  9835  infxpenlem  9896  cfub  10132  cfsuc  10140  coflim  10144  hsmexlem2  10310  ondomon  10446  pwcfsdom  10466  inar1  10658  tskord  10663  grudomon  10700  gruina  10701  sltres  27594  nosupno  27635  nosupbday  27637  noinfno  27650  oldssmade  27815  madebday  27838  mulsproplem13  28060  mulsproplem14  28061  dfrdg2  35808  aomclem6  43071  nnoeomeqom  43324  naddgeoa  43406  naddwordnexlem1  43409  naddwordnexlem4  43413  iscard5  43548