Theorem elch0

Description: Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001) (New usage is discouraged.)

	Ref	Expression
Assertion	elch0	⊢ ( 𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ )

Proof

Step	Hyp	Ref	Expression
1		df-ch0	⊢ 0ℋ = { 0ℎ }
2	1	eleq2i	⊢ ( 𝐴 ∈ 0ℋ ↔ 𝐴 ∈ { 0ℎ } )
3		ax-hv0cl	⊢ 0ℎ ∈ ℋ
4	3	elexi	⊢ 0ℎ ∈ V
5	4	elsn2	⊢ ( 𝐴 ∈ { 0ℎ } ↔ 𝐴 = 0ℎ )
6	2 5	bitri	⊢ ( 𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ )