Theorem shne0i

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

	Ref	Expression
Hypothesis	shne0.1	⊢ 𝐴 ∈ Sℋ
Assertion	shne0i	⊢ ( 𝐴 ≠ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ )

Proof

Step	Hyp	Ref	Expression
1		shne0.1	⊢ 𝐴 ∈ Sℋ
2		df-ne	⊢ ( 𝐴 ≠ 0ℋ ↔ ¬ 𝐴 = 0ℋ )
3		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 0ℋ ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 0ℋ ) )
4		nss	⊢ ( ¬ 𝐴 ⊆ 0ℋ ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 0ℋ ) )
5		shle0	⊢ ( 𝐴 ∈ Sℋ → ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ ) )
6	1 5	ax-mp	⊢ ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ )
7	6	notbii	⊢ ( ¬ 𝐴 ⊆ 0ℋ ↔ ¬ 𝐴 = 0ℋ )
8	3 4 7	3bitr2ri	⊢ ( ¬ 𝐴 = 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 0ℋ )
9		elch0	⊢ ( 𝑥 ∈ 0ℋ ↔ 𝑥 = 0ℎ )
10	9	necon3bbii	⊢ ( ¬ 𝑥 ∈ 0ℋ ↔ 𝑥 ≠ 0ℎ )
11	10	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ )
12	2 8 11	3bitri	⊢ ( 𝐴 ≠ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ )