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	|- A e. SH
Assertion	shne0i	|- ( A =/= 0H <-> E. x e. A x =/= 0h )

Proof

Step	Hyp	Ref	Expression
1		shne0.1	|- A e. SH
2		df-ne	|- ( A =/= 0H <-> -. A = 0H )
3		df-rex	|- ( E. x e. A -. x e. 0H <-> E. x ( x e. A /\ -. x e. 0H ) )
4		nss	|- ( -. A C_ 0H <-> E. x ( x e. A /\ -. x e. 0H ) )
5		shle0	|- ( A e. SH -> ( A C_ 0H <-> A = 0H ) )
6	1 5	ax-mp	|- ( A C_ 0H <-> A = 0H )
7	6	notbii	|- ( -. A C_ 0H <-> -. A = 0H )
8	3 4 7	3bitr2ri	|- ( -. A = 0H <-> E. x e. A -. x e. 0H )
9		elch0	|- ( x e. 0H <-> x = 0h )
10	9	necon3bbii	|- ( -. x e. 0H <-> x =/= 0h )
11	10	rexbii	|- ( E. x e. A -. x e. 0H <-> E. x e. A x =/= 0h )
12	2 8 11	3bitri	|- ( A =/= 0H <-> E. x e. A x =/= 0h )