Theorem cheli 31168

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

Hypothesis

Ref	Expression
chssi.1	⊢ 𝐻 ∈ Cℋ

Assertion

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

Proof of Theorem cheli

Step	Hyp	Ref	Expression
1		chssi.1	. . 3 ⊢ 𝐻 ∈ Cℋ
2	1	chssii 31167	. 2 ⊢ 𝐻 ⊆ ℋ
3	2	sseli 3945	1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Syntax hints:   → wi 4   ∈ wcel 2109   ℋchba 30855   C_ℋ cch 30865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-hilex 30935

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fv 6522  df-ov 7393  df-sh 31143  df-ch 31157

This theorem is referenced by:  pjhthlem1  31327  pjhthlem2  31328  h1de2ci  31492  spanunsni  31515  spansncvi  31588  3oalem1  31598  pjcompi  31608  pjocini  31634  pjjsi  31636  pjrni  31638  pjdsi  31648  pjds3i  31649  mayete3i  31664  riesz3i  31998  pjnmopi  32084  pjnormssi  32104  pjimai  32112  pjclem4a  32134  pjclem4  32135  pj3lem1  32142  pj3si  32143  strlem1  32186  strlem3  32189  strlem5  32191  hstrlem3  32197  hstrlem5  32199  sumdmdii  32351  sumdmdlem  32354  sumdmdlem2  32355