This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chle0i

Description: No Hilbert closed subspace is smaller than zero. (Contributed by NM, 7-Apr-2001) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ch0le.1	$⊢ A \in C_{ℋ}$
	Assertion	chle0i	$⊢ A \subseteq 0_{ℋ} \leftrightarrow A = 0_{ℋ}$

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2		chle0	$⊢ A \in C_{ℋ} \to (A \subseteq 0_{ℋ} \leftrightarrow A = 0_{ℋ})$
3	1 2	ax-mp	$⊢ A \subseteq 0_{ℋ} \leftrightarrow A = 0_{ℋ}$