Theorem sheli 30054

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

Syntax hints:   → wi 4   ∈ wcel 2106   ℋchba 29759   S_ℋ csh 29768

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 2707  ax-sep 5255  ax-hilex 29839

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 2714  df-cleq 2728  df-clel 2814  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-sh 30047

This theorem is referenced by:  norm1exi  30090  hhssabloi  30102  hhssnv  30104  shscli  30157  shunssi  30208  shmodsi  30229  omlsii  30243  5oalem1  30494  5oalem2  30495  5oalem3  30496  5oalem5  30498  imaelshi  30898  pjimai  31016  shatomici  31198  shatomistici  31201  cdjreui  31272  cdj1i  31273  cdj3lem1  31274  cdj3lem2b  31277  cdj3lem3  31278  cdj3lem3b  31280  cdj3i  31281