Definition df-le 121

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

Assertion

Ref	Expression
df-le	(a ≤2 b) = ((a ∪ 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 ∪ b)
5	4, 2	tb 5	. 2 term  ((a ∪ b) ≡ b)
6	3, 5	wb 1	1 wff  (a ≤2 b) = ((a ∪ b) ≡ b)

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

metamath.org