Definition df-le1 130

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

Hypothesis

Ref	Expression
df-le1.1	(a v b) = b

Assertion

Ref	Expression
df-le1	a =< b

Detailed syntax breakdown of Definition df-le1

Step	Hyp	Ref	Expression
1		wva	. 2 term a
2		wvb	. 2 term b
3	1, 2	wle 2	1 wff a =< b

This definition is referenced by:  df2le1 135  bltr 138  bile 142  le1 146  le0 147  ler 149  leror 152  lea 160  comcom 453  biao 799  oale 829  oau 929  oa23 936  lem4.6.6i1j3 1091  com3iia 1099  lem4.6.7 1100

Copyright terms: Public domain