Definition df-c2 133

Description: Define 'commutes'. See df-c1 132 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 181  cbtr 182  comcom2 183  wwcomd 214  wcom0 407  wcom1 408  comcom 453  comd 456  comcom5 458  com2or 483  comcmtr1 494  comi1 709

Copyright terms: Public domain