Metamath Proof Explorer

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 ⊢ S linIndS M → S ∈ V ∧ M ∈ V

Proof

Step Hyp Ref Expression
1 rellininds ⊢ Rel ⁡ linIndS
2 1 brrelex12i ⊢ S linIndS M → S ∈ V ∧ M ∈ V