Theorem sheli 29096

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 29095	. 2 ⊢ 𝐻 ⊆ ℋ
3	2	sseli 3888	1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Syntax hints:   → wi 4   ∈ wcel 2111   ℋchba 28801   S_ℋ csh 28810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-hilex 28881

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-v 3411  df-un 3863  df-in 3865  df-ss 3875  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-br 5033  df-opab 5095  df-xp 5530  df-cnv 5532  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-sh 29089

This theorem is referenced by:  norm1exi  29132  hhssabloi  29144  hhssnv  29146  shscli  29199  shunssi  29250  shmodsi  29271  omlsii  29285  5oalem1  29536  5oalem2  29537  5oalem3  29538  5oalem5  29540  imaelshi  29940  pjimai  30058  shatomici  30240  shatomistici  30243  cdjreui  30314  cdj1i  30315  cdj3lem1  30316  cdj3lem2b  30319  cdj3lem3  30320  cdj3lem3b  30322  cdj3i  30323