Theorem linindsv

Description: The classes of the module and its linearly independent subsets are sets. (Contributed by AV, 13-Apr-2019)

	Ref	Expression
Assertion	linindsv	⊢ ( 𝑆 linIndS 𝑀 → ( 𝑆 ∈ V ∧ 𝑀 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		rellininds	⊢ Rel linIndS
2	1	brrelex12i	⊢ ( 𝑆 linIndS 𝑀 → ( 𝑆 ∈ V ∧ 𝑀 ∈ V ) )