Theorem chssii 31838

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

This proof depends on syntax axioms:   ∈ wcel 2144   ⊆ wss 3895   ℋchba 31526   C_ℋ cch 31536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-hilex 31606

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fv 6546  df-ov 7423  df-sh 31814  df-ch 31828

This theorem is used by:  cheli  31839  chelii  31840  hhsscms  31885  chocvali  31906  chm1i  32063  chsscon3i  32068  chsscon2i  32070  chjoi  32095  chj1i  32096  shjshsi  32099  sshhococi  32153  h1dei  32157  spansnpji  32185  spanunsni  32186  h1datomi  32188  spansnji  32253  pjfi  32311  riesz3i  32669  hmopidmpji  32759  pjoccoi  32785  pjinvari  32798  stcltr2i  32882  mdsymi  33018  mdcompli  33036  dmdcompli  33037