Definition df-le 129

Description: Define "less than or equal to" analogue. (Contributed by NM, 27-Aug-1997.)

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 10	. 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  346  wdf-le1  378  wdf-le2  379  wle0  390  wler  391