Theorem chssii 31561

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

Syntax hints:   ∈ wcel 2143   ⊆ wss 3906   ℋchba 31249   C_ℋ cch 31259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-hilex 31329

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fv 6546  df-ov 7415  df-sh 31537  df-ch 31551

This theorem is referenced by:  cheli  31562  chelii  31563  hhsscms  31608  chocvali  31629  chm1i  31786  chsscon3i  31791  chsscon2i  31793  chjoi  31818  chj1i  31819  shjshsi  31822  sshhococi  31876  h1dei  31880  spansnpji  31908  spanunsni  31909  h1datomi  31911  spansnji  31976  pjfi  32034  riesz3i  32392  hmopidmpji  32482  pjoccoi  32508  pjinvari  32521  stcltr2i  32605  mdsymi  32741  mdcompli  32759  dmdcompli  32760