Definition df-lindeps

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

	Ref	Expression
Assertion	df-lindeps	$$⊢\mathrm{linDepS}=\left\{⟨s,m⟩|\neg s\mathrm{linIndS}m\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clindeps	$$class\mathrm{linDepS}$$
1		vs	$$setvars$$
2		vm	$$setvarm$$
3	1	cv	$$setvars$$
4		clininds	$$class\mathrm{linIndS}$$
5	2	cv	$$setvarm$$
6	3 5 4	wbr	$$wffs\mathrm{linIndS}m$$
7	6	wn	$$wff\neg s\mathrm{linIndS}m$$
8	7 1 2	copab	$$class\left\{⟨s,m⟩|\neg s\mathrm{linIndS}m\right\}$$
9	0 8	wceq	$$wff\mathrm{linDepS}=\left\{⟨s,m⟩|\neg s\mathrm{linIndS}m\right\}$$