Definition df-c2 133

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

Hypothesis

Ref	Expression
df-c2.1	a C b

Assertion

Ref	Expression
df-c2	a = ((a ∩ b) ∪ (a ∩ b⊥ ))

Detailed syntax breakdown of Definition df-c2

Step	Hyp	Ref	Expression
1		wva	. 2 term  a
2		wvb	. . . 4 term  b
3	1, 2	wa 7	. . 3 term  (a ∩ b)
4	2	wn 4	. . . 4 term  b⊥
5	1, 4	wa 7	. . 3 term  (a ∩ b⊥ )
6	3, 5	wo 6	. 2 term  ((a ∩ b) ∪ (a ∩ b⊥ ))
7	1, 6	wb 1	1 wff  a = ((a ∩ b) ∪ (a ∩ b⊥ ))

This definition is referenced by:  bctr  181  cbtr  182  comcom2  183  wwcomd  214  wcom0  407  wcom1  408  comcom  453  comd  456  comcom5  458  com2or  483  comcmtr1  494  comi1  709