Theorem sheli 30276

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

Syntax hints:   → wi 4   ∈ wcel 2106   ℋchba 29981   S_ℋ csh 29990

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5287  ax-hilex 30061

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3429  df-v 3471  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-nul 4314  df-if 4518  df-pw 4593  df-sn 4618  df-pr 4620  df-op 4624  df-br 5137  df-opab 5199  df-xp 5670  df-cnv 5672  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-sh 30269

This theorem is referenced by:  norm1exi  30312  hhssabloi  30324  hhssnv  30326  shscli  30379  shunssi  30430  shmodsi  30451  omlsii  30465  5oalem1  30716  5oalem2  30717  5oalem3  30718  5oalem5  30720  imaelshi  31120  pjimai  31238  shatomici  31420  shatomistici  31423  cdjreui  31494  cdj1i  31495  cdj3lem1  31496  cdj3lem2b  31499  cdj3lem3  31500  cdj3lem3b  31502  cdj3i  31503