Theorem comor2 444

Description: Commutation law.

Assertion

Ref	Expression
comor2	(a ∪ b) C b

Proof of Theorem comor2

Step	Hyp	Ref	Expression
1		ax-a2 30	. 2 (a ∪ b) = (b ∪ a)
2		comor1 443	. 2 (b ∪ a) C b
3	1, 2	bctr 173	1 (a ∪ b) C b

Syntax hints:   C wc 3   ∪ wo 6

This theorem is referenced by:  comorr2 445  oml6 470  gsth2 472  dfi3b 481  i3con 533  i3orlem7 540  i3orlem8 541  ud1lem3 544  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem3d 557  ud3lem3 558  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem3b 566  ud4lem3 567  ud5lem1 571  ud5lem3 576  u4lemana 590  u4lemoa 605  u4lemona 610  u3lemob 614  u3lemonb 619  u4lemle2 700  u4lem1 719  u4lem5 746  u4lem6 750  u1lem11 762  u3lem11 768  u3lem15 777  test 784  test2 785  3vded21 799  neg3antlem2 847  mhlem 858  mhlem1 859

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

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

metamath.org