Theorem shssii 28974

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
shssi.1	⊢ 𝐻 ∈ Sℋ

Assertion

Ref	Expression
shssii	⊢ 𝐻 ⊆ ℋ

Proof of Theorem shssii

Step	Hyp	Ref	Expression
1		shssi.1	. 2 ⊢ 𝐻 ∈ Sℋ
2		shss 28971	. 2 ⊢ (𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ)
3	1, 2	ax-mp 5	1 ⊢ 𝐻 ⊆ ℋ

Syntax hints:   ∈ wcel 2114   ⊆ wss 3924   ℋchba 28680   S_ℋ csh 28689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-hilex 28760

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3488  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-br 5053  df-opab 5115  df-xp 5547  df-cnv 5549  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-sh 28968

This theorem is referenced by:  sheli  28975  shelii  28976  chssii  28992  hhssabloilem  29022  hhssabloi  29023  hhssnv  29025  hhssba  29032  shunssji  29130  shsval3i  29149  shjshsi  29253  span0  29303  spanuni  29305  imaelshi  29819  nlelchi  29822  hmopidmchi  29912  pjimai  29937  shatomistici  30122