Theorem onelss 6437

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3976  Ord word 6394  Oncon0 6395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-ss 3993  df-uni 4932  df-tr 5284  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399

This theorem is referenced by:  ordunidif  6444  onelssi  6510  ssorduni  7814  sucexeloniOLD  7846  suceloniOLD  7848  tfisi  7896  poseq  8199  tfrlem9  8441  tfrlem11  8444  oaordex  8614  oaass  8617  odi  8635  omass  8636  oewordri  8648  nnaordex  8694  domtriord  9189  hartogs  9613  card2on  9623  tskwe  10019  infxpenlem  10082  cfub  10318  cfsuc  10326  coflim  10330  hsmexlem2  10496  ondomon  10632  pwcfsdom  10652  inar1  10844  tskord  10849  grudomon  10886  gruina  10887  sltres  27725  nosupno  27766  nosupbday  27768  noinfno  27781  oldssmade  27934  madebday  27956  mulsproplem13  28172  mulsproplem14  28173  dfrdg2  35759  aomclem6  43016  nnoeomeqom  43274  naddgeoa  43356  naddwordnexlem1  43359  naddwordnexlem4  43363  iscard5  43498