Theorem chssii 31317

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 31313	. 2 ⊢ 𝐻 ∈ Sℋ
3	2	shssii 31299	1 ⊢ 𝐻 ⊆ ℋ

Syntax hints:   ∈ wcel 2114   ⊆ wss 3890   ℋchba 31005   C_ℋ cch 31015

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-hilex 31085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fv 6500  df-ov 7363  df-sh 31293  df-ch 31307

This theorem is referenced by:  cheli  31318  chelii  31319  hhsscms  31364  chocvali  31385  chm1i  31542  chsscon3i  31547  chsscon2i  31549  chjoi  31574  chj1i  31575  shjshsi  31578  sshhococi  31632  h1dei  31636  spansnpji  31664  spanunsni  31665  h1datomi  31667  spansnji  31732  pjfi  31790  riesz3i  32148  hmopidmpji  32238  pjoccoi  32264  pjinvari  32277  stcltr2i  32361  mdsymi  32497  mdcompli  32515  dmdcompli  32516