Theorem sheli 28991

Description: A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)

Hypothesis

Ref	Expression
shssi.1	⊢ 𝐻 ∈ Sℋ

Assertion

Ref	Expression
sheli	⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Proof of Theorem sheli

Step	Hyp	Ref	Expression
1		shssi.1	. . 3 ⊢ 𝐻 ∈ Sℋ
2	1	shssii 28990	. 2 ⊢ 𝐻 ⊆ ℋ
3	2	sseli 3963	1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Syntax hints:   → wi 4   ∈ wcel 2114   ℋchba 28696   S_ℋ csh 28705

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 5203  ax-hilex 28776

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 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-sh 28984

This theorem is referenced by:  norm1exi  29027  hhssabloi  29039  hhssnv  29041  shscli  29094  shunssi  29145  shmodsi  29166  omlsii  29180  5oalem1  29431  5oalem2  29432  5oalem3  29433  5oalem5  29435  imaelshi  29835  pjimai  29953  shatomici  30135  shatomistici  30138  cdjreui  30209  cdj1i  30210  cdj3lem1  30211  cdj3lem2b  30214  cdj3lem3  30215  cdj3lem3b  30217  cdj3i  30218