shne0i

Description: A nonzero subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	shne0.1	$⊢ A \in S_{ℋ}$
	Assertion	shne0i	$⊢ A \neq 0_{ℋ} \leftrightarrow \exists x \in A x \neq 0_{ℎ}$

Step	Hyp	Ref	Expression
1		shne0.1	$⊢ A \in S_{ℋ}$
2		df-ne	$⊢ A \neq 0_{ℋ} \leftrightarrow \neg A = 0_{ℋ}$
3		df-rex	$⊢ \exists x \in A \neg x \in 0_{ℋ} \leftrightarrow \exists x (x \in A \land \neg x \in 0_{ℋ})$
4		nss	$⊢ \neg A \subseteq 0_{ℋ} \leftrightarrow \exists x (x \in A \land \neg x \in 0_{ℋ})$
5		shle0	$⊢ A \in S_{ℋ} \to (A \subseteq 0_{ℋ} \leftrightarrow A = 0_{ℋ})$
6	1 5	ax-mp	$⊢ A \subseteq 0_{ℋ} \leftrightarrow A = 0_{ℋ}$
7	6	notbii	$⊢ \neg A \subseteq 0_{ℋ} \leftrightarrow \neg A = 0_{ℋ}$
8	3 4 7	3bitr2ri	$⊢ \neg A = 0_{ℋ} \leftrightarrow \exists x \in A \neg x \in 0_{ℋ}$
9		elch0	$⊢ x \in 0_{ℋ} \leftrightarrow x = 0_{ℎ}$
10	9	necon3bbii	$⊢ \neg x \in 0_{ℋ} \leftrightarrow x \neq 0_{ℎ}$
11	10	rexbii	$⊢ \exists x \in A \neg x \in 0_{ℋ} \leftrightarrow \exists x \in A x \neq 0_{ℎ}$
12	2 8 11	3bitri	$⊢ A \neq 0_{ℋ} \leftrightarrow \exists x \in A x \neq 0_{ℎ}$

Metamath Proof Explorer