Theorem linds1

Description: An independent set of vectors is a set of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypothesis	islinds.b	|- B = ( Base ` W )
Assertion	linds1	|- ( X e. ( LIndS ` W ) -> X C_ B )

Proof

Step	Hyp	Ref	Expression
1		islinds.b	|- B = ( Base ` W )
2		elfvdm	|- ( X e. ( LIndS ` W ) -> W e. dom LIndS )
3	1	islinds	|- ( W e. dom LIndS -> ( X e. ( LIndS ` W ) <-> ( X C_ B /\ ( _I |` X ) LIndF W ) ) )
4	2 3	syl	|- ( X e. ( LIndS ` W ) -> ( X e. ( LIndS ` W ) <-> ( X C_ B /\ ( _I |` X ) LIndF W ) ) )
5	4	ibi	|- ( X e. ( LIndS ` W ) -> ( X C_ B /\ ( _I |` X ) LIndF W ) )
6	5	simpld	|- ( X e. ( LIndS ` W ) -> X C_ B )