Definition df-le1 122

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

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 127  bltr 130  bile 134  le1 138  le0 139  ler 141  leror 144  lea 152  comcom 435  biao 781  oale 811  oau 909  oa23 916

metamath.org