Definition df-le2 123

Description: Define 'less than or equal to'. See df-le1 122 for the other direction.

Hypothesis

Ref	Expression
df-le2.1	a =< b

Assertion

Ref	Expression
df-le2	(a v 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 v b)
4	3, 2	wb 1	1 wff (a v b) = b

This definition is referenced by:  df2le2 128  letr 129  bltr 130  lebi 137  ler 141  leror 144  lecon 146  wwoml2 204  sklem 222  nom13 302  nom14 303  nom15 304  wr5 413  oml2 433  gsth 471  cmtr1com 475  i0cmtrcom 477  df2i3 480  oi3ai3 485  i3con 533  i3orlem6 539  ud3lem1c 550  ud3lem3 558  ud4lem1c 561  ud4lem1 563  ud4lem3b 566  ud5lem1 571  u3lemoa 604  u2lemona 608  u3lemona 609  u4lemona 610  u5lemona 611  u1lemob 612  u3lemob 614  u4lemob 615  u5lemob 616  u3lemonb 619  u4lemonb 620  u5lemonb 621  u4lem1 719  u4lem2 729  u4lem5 746  u4lem6 750  u24lem 752  u3lem13a 771  u3lem13b 772  biao 781  test 784  test2 785  3vth3 788  3vth6 791  orbi 824  elimconslem 849  elimcons 850  elimcons2 851  comanblem1 852  mhlem 858  gomaex3lem1 894  oaidlem2 911  oaidlem2g 912  oa3-6lem 960  oa3-u1lem 965  oa3-u2lem 966  oa3-u1 971  oa3-u2 972  oadistc0 1001

metamath.org