Definition df-le 121

Description: Define 'less than or equal to' analogue.

Assertion

Ref	Expression
df-le	(a =<2 b) = ((a v b) == b)

Detailed syntax breakdown of Definition df-le

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . 3 term b
3	1, 2	wle2 11	. 2 term (a =<2 b)
4	1, 2	wo 6	. . 3 term (a v b)
5	4, 2	tb 5	. 2 term ((a v b) == b)
6	3, 5	wb 1	1 wff (a =<2 b) = ((a v b) == b)

This definition is referenced by:  lei2 338  wdf-le1 360  wdf-le2 361  wle0 372  wler 373

metamath.org