Definition df-le2 131

Description: Define "less than or equal to". See df-le1 130 for the other direction. (Contributed by NM, 27-Aug-1997.)

Hypothesis

Ref	Expression
df-le2.1	a ≤ b

Assertion

Ref	Expression
df-le2	(a ∪ b) = b

Detailed syntax breakdown of Definition df-le2

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wo 6	. 2 term  (a ∪ b)
4	3, 2	wb 1	1 wff  (a ∪ b) = b

This definition is referenced by:  df2le2  136  letr  137  bltr  138  lebi  145  ler  149  leror  152  lecon  154  wwoml2  212  sklem  230  nom13  310  nom14  311  nom15  312  k1-4  359  oml2  451  gsth  489  cmtr1com  493  i0cmtrcom  495  df2i3  498  oi3ai3  503  i3con  551  i3orlem6  557  ud3lem1c  568  ud3lem3  576  ud4lem1c  579  ud4lem1  581  ud4lem3b  584  ud5lem1  589  u3lemoa  622  u2lemona  626  u3lemona  627  u4lemona  628  u5lemona  629  u1lemob  630  u3lemob  632  u4lemob  633  u5lemob  634  u3lemonb  637  u4lemonb  638  u5lemonb  639  u4lem1  737  u4lem2  747  u4lem5  764  u4lem6  768  u24lem  770  u3lem13a  789  u3lem13b  790  biao  799  test  802  test2  803  3vth3  806  3vth6  809  orbi  842  elimconslem  867  elimcons  868  elimcons2  869  comanblem1  870  mhlem  876  e2ast2  894  gomaex3lem1  914  oaidlem2  931  oaidlem2g  932  oa3-6lem  980  oa3-u1lem  985  oa3-u2lem  986  oa3-u1  991  oa3-u2  992  oadistc0  1021  lem3.3.7i2e2  1064  lem3.3.7i3e2  1067  lem4.6.2e1  1082  lem4.6.6i1j0  1092  lem4.6.6i1j3  1094  lem4.6.6i2j0  1095  lem4.6.6i3j0  1098  lem4.6.6i4j0  1100  lem4.6.7  1103  ml2i  1125  vneulem12  1142  vneulemexp  1148  dp53lemc  1165  dp53lemf  1168  dp35lemc  1175  dp41leml  1193  dp32  1196  xdp41  1198  xdp53  1200  xxdp41  1201  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemc  1211