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	⊢ ≤ = ((ℝ × ℝ) ∖ ◡ < )

Detailed syntax breakdown of Definition df-le

Step	Hyp	Ref	Expression
1		cle 4092	. 2 class ≤
2		cr 4027	. . . 4 class ℝ
3	2, 2	cxp 2408	. . 3 class (ℝ × ℝ)
4		clt 4033	. . . 4 class <
5	4	ccnv 2409	. . 3 class ◡ <
6	3, 5	cdif 1484	. 2 class ((ℝ × ℝ) ∖ ◡ < )
7	1, 6	wceq 1091	1 wff ≤ = ((ℝ × ℝ) ∖ ◡ < )

This definition is referenced by:  leltt 4278

metamath.org