Theorem chssii 29881

Description: A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)

Hypothesis

Ref	Expression
chssi.1	⊢ 𝐻 ∈ Cℋ

Assertion

Ref	Expression
chssii	⊢ 𝐻 ⊆ ℋ

Proof of Theorem chssii

Step	Hyp	Ref	Expression
1		chssi.1	. . 3 ⊢ 𝐻 ∈ Cℋ
2	1	chshii 29877	. 2 ⊢ 𝐻 ∈ Sℋ
3	2	shssii 29863	1 ⊢ 𝐻 ⊆ ℋ

Syntax hints:   ∈ wcel 2106   ⊆ wss 3902   ℋchba 29569   C_ℋ cch 29579

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 2708  ax-sep 5248  ax-hilex 29649

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3444  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-br 5098  df-opab 5160  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6436  df-fv 6492  df-ov 7345  df-sh 29857  df-ch 29871

This theorem is referenced by:  cheli  29882  chelii  29883  hhsscms  29928  chocvali  29949  chm1i  30106  chsscon3i  30111  chsscon2i  30113  chjoi  30138  chj1i  30139  shjshsi  30142  sshhococi  30196  h1dei  30200  spansnpji  30228  spanunsni  30229  h1datomi  30231  spansnji  30296  pjfi  30354  riesz3i  30712  hmopidmpji  30802  pjoccoi  30828  pjinvari  30841  stcltr2i  30925  mdsymi  31061  mdcompli  31079  dmdcompli  31080