Theorem comorr 184

Description: Commutation law. Does not use OML. (Contributed by NM, 30-Aug-1997.)

Assertion

Ref	Expression
comorr	a C (a ∪ b)

Proof of Theorem comorr

Step	Hyp	Ref	Expression
1		leo 158	. 2 a ≤ (a ∪ b)
2	1	lecom 180	1 a C (a ∪ b)

Syntax hints:   C wc 3   ∪ wo 6

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

This theorem depends on definitions:  df-a 40  df-le1 130  df-le2 131  df-c1 132

This theorem is referenced by:  comid  187  comor1  461  nbdi  486  df2i3  498  i3lem1  504  i3con  551  ud1lem1  560  ud1lem3  562  ud3lem1c  568  ud3lem2  571  ud3lem3  576  ud4lem1c  579  ud4lem1  581  ud4lem2  582  ud5lem3b  592  ud5lem3  594  u3lemaa  602  u3lemana  607  u4lem1  737  u3lem10  785  u3lem13a  789  u3lem13b  790  i1abs  801  3vth5  808  mhlem1  877  marsdenlem1  880  marsdenlem2  881  oau  929  oa23  936  lem4.6.2e1  1082