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 e. _V /\ M e. _V ) )

Proof

Step Hyp Ref Expression
1 rellininds 
 |-  Rel linIndS
2 1 brrelex12i 
 |-  ( S linIndS M -> ( S e. _V /\ M e. _V ) )