Definition df-c2 125

Description: Define 'commutes'. See df-c1 124 for the other direction.

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 173  cbtr 174  comcom2 175  wwcomd 206  wcom0 389  wcom1 390  comcom 435  comd 438  comcom5 440  com2or 465  comcmtr1 476  comi1 691

metamath.org