Definition df-le2 131

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

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 1063  lem3.3.7i3e2 1066  lem4.6.2e1 1079  lem4.6.6i1j0 1089  lem4.6.6i1j3 1091  lem4.6.6i2j0 1092  lem4.6.6i3j0 1095  lem4.6.6i4j0 1097  lem4.6.7 1100

Copyright terms: Public domain