Definition df-lindeps 45458

Description: Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.)

Assertion

Ref	Expression
df-lindeps	⊢ linDepS = {⟨𝑠, 𝑚⟩ ∣ ¬ 𝑠 linIndS 𝑚}

Distinct variable group:   𝑚,𝑠

Detailed syntax breakdown of Definition df-lindeps

Step	Hyp	Ref	Expression
1		clindeps 45455	. 2 class linDepS
2		vs	. . . . . 6 setvar 𝑠
3	2	cv 1542	. . . . 5 class 𝑠
4		vm	. . . . . 6 setvar 𝑚
5	4	cv 1542	. . . . 5 class 𝑚
6		clininds 45454	. . . . 5 class linIndS
7	3, 5, 6	wbr 5053	. . . 4 wff 𝑠 linIndS 𝑚
8	7	wn 3	. . 3 wff ¬ 𝑠 linIndS 𝑚
9	8, 2, 4	copab 5115	. 2 class {⟨𝑠, 𝑚⟩ ∣ ¬ 𝑠 linIndS 𝑚}
10	1, 9	wceq 1543	1 wff linDepS = {⟨𝑠, 𝑚⟩ ∣ ¬ 𝑠 linIndS 𝑚}

This definition is referenced by:  lindepsnlininds  45466