Theorem df2le2 128

Description: Alternate definition of 'less than or equal to'.

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 123	. 2 (a ∪ b) = b
3	2	leoa 115	1 (a ∩ b) = a

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

This theorem is referenced by:  lbtr 131  lel 143  leran 145  lecom 172  lei3 238  nom20 305  nom21 306  nom22 307  nom23 308  nom24 309  wdf-c2 366  gsth 471  dfi3b 481  lem4 493  ud3lem1a 548  ud3lem1d 551  ud3lem3a 554  ud3lem3d 557  ud4lem1a 559  ud4lem1b 560  ud4lem3a 565  ud5lem1b 569  u3lemana 589  u4lemana 590  u4lemab 595  u5lemab 596  i1com 690  u4lem5 746  u4lem6 750  u24lem 752  u1lem8 758  u3lem15 777  bi1o1a 780  biao 781  imp3 823  mlaconj4 826  elimcons2 851  comanblem1 852  mhlem 858  mhlem1 859  mlaconjolem 867  gomaex3lem9 902  oas 905  oagen1b 995  oadistb 1000  oadistc0 1001  oadistc 1002  oadistd 1003  4oagen1b 1022  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-le2 123

metamath.org