Theorem comid 179

Description: Identity law for commutation. Does not use OML.

Assertion

Ref	Expression
comid	a C a

Proof of Theorem comid

Step	Hyp	Ref	Expression
1		comorr 176	. 2 a C (a ∪ a)
2		oridm 102	. 2 (a ∪ a) = a
3	1, 2	cbtr 174	1 a C a

Syntax hints:   C wc 3   ∪ wo 6

This theorem is referenced by:  comi32 492  i3abs3 506  ud1lem2 543  ud1lem3 544  ud2lem3 547  ud4lem2 564  ud4lem3 567  u1lemaa 582  u3lemaa 584  u3lemana 589  u2lemanb 598  u4lemanb 600  u4lemob 615  u1lemc1 662  u2lemc1 663  u4lemc1 665  u1lemc3 673  u2lemc5 679  u4lemc5 681  u1lemc4 683  u3lemc4 685  u4lemc4 686  u5lemc4 687  u3lem2 728  u1lem4 739  u4lem4 741  u3lem13a 771  bi1o1a 780  3vded21 799  3vded3 801  1oa 802  mhlem1 859  marsdenlem2 863  gomaex3lem1 894  gomaex3lem2 895  gomaex3lem3 896  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org