Theorem sheli 31273

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

Syntax hints:   → wi 4   ∈ wcel 2114   ℋchba 30978   S_ℋ csh 30987

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220  ax-hilex 31058

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-cnv 5628  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-sh 31266

This theorem is referenced by:  norm1exi  31309  hhssabloi  31321  hhssnv  31323  shscli  31376  shunssi  31427  shmodsi  31448  omlsii  31462  5oalem1  31713  5oalem2  31714  5oalem3  31715  5oalem5  31717  imaelshi  32117  pjimai  32235  shatomici  32417  shatomistici  32420  cdjreui  32491  cdj1i  32492  cdj3lem1  32493  cdj3lem2b  32496  cdj3lem3  32497  cdj3lem3b  32499  cdj3i  32500