Theorem chssii 31167

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3917   ℋchba 30855   C_ℋ cch 30865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-hilex 30935

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fv 6522  df-ov 7393  df-sh 31143  df-ch 31157

This theorem is referenced by:  cheli  31168  chelii  31169  hhsscms  31214  chocvali  31235  chm1i  31392  chsscon3i  31397  chsscon2i  31399  chjoi  31424  chj1i  31425  shjshsi  31428  sshhococi  31482  h1dei  31486  spansnpji  31514  spanunsni  31515  h1datomi  31517  spansnji  31582  pjfi  31640  riesz3i  31998  hmopidmpji  32088  pjoccoi  32114  pjinvari  32127  stcltr2i  32211  mdsymi  32347  mdcompli  32365  dmdcompli  32366