Definition df-le 4277

Description: Define 'less than or equal to' on real subset of complex numbers. Theorem leloet 4284 relates it to 'less than'.

Assertion

Ref	Expression
df-le	|- <_ = ((RR X. RR) \ `' < )

Detailed syntax breakdown of Definition df-le

Step	Hyp	Ref	Expression
1		cle 4092	. 2 class <_
2		cr 4027	. . . 4 class RR
3	2, 2	cxp 2408	. . 3 class (RR X. RR)
4		clt 4033	. . . 4 class <
5	4	ccnv 2409	. . 3 class `' <
6	3, 5	cdif 1484	. 2 class ((RR X. RR) \ `' < )
7	1, 6	wceq 1091	1 wff <_ = ((RR X. RR) \ `' < )

This definition is referenced by:  leltt 4278

metamath.org