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	$$⊢A\in 0_{\mathscr{H}}\leftrightarrow A=0_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		df-ch0	$$⊢0_{\mathscr{H}}=\left\{0_{ℎ}\right\}$$
2	1	eleq2i	$$⊢A\in 0_{\mathscr{H}}\leftrightarrow A\in \left\{0_{ℎ}\right\}$$
3		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
4	3	elexi	$$⊢0_{ℎ}\in \mathrm{V}$$
5	4	elsn2	$$⊢A\in \left\{0_{ℎ}\right\}\leftrightarrow A=0_{ℎ}$$
6	2 5	bitri	$$⊢A\in 0_{\mathscr{H}}\leftrightarrow A=0_{ℎ}$$