Theorem onelss 6406

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3948  Ord word 6363  Oncon0 6364

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368

This theorem is referenced by:  ordunidif  6413  onelssi  6479  ssorduni  7768  sucexeloniOLD  7800  suceloniOLD  7802  tfisi  7850  poseq  8146  tfrlem9  8387  tfrlem11  8390  oaordex  8560  oaass  8563  odi  8581  omass  8582  oewordri  8594  nnaordex  8640  domtriord  9125  hartogs  9541  card2on  9551  tskwe  9947  infxpenlem  10010  cfub  10246  cfsuc  10254  coflim  10258  hsmexlem2  10424  ondomon  10560  pwcfsdom  10580  inar1  10772  tskord  10777  grudomon  10814  gruina  10815  sltres  27389  nosupno  27430  nosupbday  27432  noinfno  27445  oldssmade  27597  madebday  27619  mulsproplem13  27811  mulsproplem14  27812  dfrdg2  35059  aomclem6  42103  nnoeomeqom  42364  naddgeoa  42447  naddwordnexlem1  42450  naddwordnexlem4  42454  iscard5  42589