Definition df-le1 130

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

Hypothesis

Ref	Expression
df-le1.1	(a ∪ 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  1094  com3iia  1102  lem4.6.7  1103