Definition df-c1 132

Description: Define "commutes". See df-c2 133 for the other direction. (Contributed by NM, 27-Aug-1997.)

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  178  comm1  179  lecom  180  bctr  181  cbtr  182  comcom2  183  comcom  453  comcom5  458  comdr  466  com3i  467  df2c1  468  com2or  483  cmtr1com  493  i0cmtrcom  495  i3lem2  505  i1com  708