Metamath Proof Explorer


Theorem rellindf

Description: The independent-family predicate is a proper relation and can be used with brrelex1i . (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Assertion rellindf Rel LIndF

Proof

Step Hyp Ref Expression
1 df-lindf LIndF = f w | f : dom f Base w [˙ Scalar w / s]˙ x dom f k Base s 0 s ¬ k w f x LSpan w f dom f x
2 1 relopabiv Rel LIndF