Definition df-c1 124

Description: Define 'commutes'. See df-c2 125 for the other direction.

Hypothesis

Ref	Expression
df-c1.1	a = ((a ∩ b) ∪ (a ∩ b⊥ ))

Assertion

Ref	Expression
df-c1	a C b

Detailed syntax breakdown of Definition df-c1

Step	Hyp	Ref	Expression
1		wva	. 2 term  a
2		wvb	. 2 term  b
3	1, 2	wc 3	1 wff  a C b

This definition is referenced by:  comm0 170  comm1 171  lecom 172  bctr 173  cbtr 174  comcom2 175  comcom 435  comcom5 440  comdr 448  com3i 449  df2c1 450  com2or 465  cmtr1com 475  i0cmtrcom 477  i3lem2 487  i1com 690

metamath.org