Theorem df2le2 136

Description: Alternate definition of "less than or equal to". (Contributed by NM, 27-Aug-1997.)

Hypothesis

Ref	Expression
df2le2.1	a ≤ b

Assertion

Ref	Expression
df2le2	(a ∩ b) = a

Proof of Theorem df2le2

Step	Hyp	Ref	Expression
1		df2le2.1	. . 3 a ≤ b
2	1	df-le2 131	. 2 (a ∪ b) = b
3	2	leoa 123	1 (a ∩ b) = a

Syntax hints:   = wb 1   ≤ wle 2   ∩ wa 7

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-le2 131

This theorem is referenced by:  lbtr  139  lel  151  leran  153  lecom  180  lei3  246  nom20  313  nom21  314  nom22  315  nom23  316  nom24  317  k1-8a  355  k1-4  359  wdf-c2  384  gsth  489  dfi3b  499  lem4  511  ud3lem1a  566  ud3lem1d  569  ud3lem3a  572  ud3lem3d  575  ud4lem1a  577  ud4lem1b  578  ud4lem3a  583  ud5lem1b  587  u3lemana  607  u4lemana  608  u4lemab  613  u5lemab  614  i1com  708  u4lem5  764  u4lem6  768  u24lem  770  u1lem8  776  u3lem15  795  bi1o1a  798  biao  799  imp3  841  mlaconj4  844  elimcons2  869  comanblem1  870  mhlem  876  mhlem1  877  mlaconjolem  885  e2ast2  894  e2astlem1  895  gomaex3lem9  922  oas  925  oagen1b  1015  oadistb  1020  oadistc0  1021  oadistc  1022  oadistd  1023  4oagen1b  1043  4oadist  1044  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  dp41lema  1182  dp41lemb  1183  xdp41  1198  xxdp41  1201  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216