Theorem leo 150

Description: L.e. absorption.

Assertion

Ref	Expression
leo	a ≤ (a ∪ b)

Proof of Theorem leo

Step	Hyp	Ref	Expression
1		a5c 113	. 2 (a ∩ (a ∪ b)) = a
2	1	df2le1 127	1 a ≤ (a ∪ b)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem is referenced by:  leor 151  leao1 154  leao2 155  ledio 168  comorr 176  distlem 180  womao 212  womaon 213  womaa 214  womaan 215  anorabs2 216  ka4lemo 220  bina3 276  bina4 277  nom14 303  nom21 306  nom22 307  nom24 309  i1or 337  i5lei4 342  2vwomlem 347  wr5-2v 348  ska2 414  gsth 471  i3bi 478  df2i3 480  dfi3b 481  oi3ai3 485  i3th8 532  i3con 533  i3orlem2 535  i3orlem4 537  i3orlem5 538  i3orlem7 540  ud3lem1a 548  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud5lem1b 569  ud5lem1 571  u4lemana 590  u4lemona 610  u3lemob 614  u1lemc6 688  comi12 689  i2bi 704  u12lembi 708  u4lem1 719  u4lem6 750  u12lem 753  u1lem8 758  u1lem9b 760  u3lem13b 772  bi1o1a 780  test2 785  3vth6 791  3vded11 796  3vded12 797  2oalem1 807  mlalem 814  sadm3 820  bi3 821  orbi 824  negantlem1 830  negantlem2 831  negantlem3 832  negantlem9 841  neg3antlem1 846  neg3antlem2 847  comanb 854  mhlemlem1 856  mhlem 858  mh 861  cancellem 873  gomaex3h3 884  gomaex3lem10 903  oas 905  oatr 908  oau 909  oa23 916  oa4lem1 917  distoah2 921  distoah4 923  oa3to4lem1 925  oa6to4h1 935  oa6to4h2 936  oa6to4h3 937  oa4to6lem1 940  oa4btoc 946  oa3-6lem 960  oa3-u1lem 965  oa3-2to2s 970  d3oa 975  d4oa 976  oaliv 983  oadist2a 987  mloa 998  oadistd 1003  axoa4a 1016  4oadist 1023

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-le1 122

metamath.org