Definition df-lindeps 45737

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 45734	. 2 class linDepS
2		vs	. . . . . 6 setvar 𝑠
3	2	cv 1540	. . . . 5 class 𝑠
4		vm	. . . . . 6 setvar 𝑚
5	4	cv 1540	. . . . 5 class 𝑚
6		clininds 45733	. . . . 5 class linIndS
7	3, 5, 6	wbr 5078	. . . 4 wff 𝑠 linIndS 𝑚
8	7	wn 3	. . 3 wff ¬ 𝑠 linIndS 𝑚
9	8, 2, 4	copab 5140	. 2 class {⟨𝑠, 𝑚⟩ ∣ ¬ 𝑠 linIndS 𝑚}
10	1, 9	wceq 1541	1 wff linDepS = {⟨𝑠, 𝑚⟩ ∣ ¬ 𝑠 linIndS 𝑚}

This definition is referenced by:  lindepsnlininds  45745