Theorem leex

Description: The less-than-or-equal-to relation is a set. (Contributed by SN, 5-Jun-2025)

	Ref	Expression
Assertion	leex	⊢ ≤ ∈ V

Proof

Step	Hyp	Ref	Expression
1		xrex	⊢ ℝ* ∈ V
2	1 1	xpex	⊢ ( ℝ* × ℝ* ) ∈ V
3		lerelxr	⊢ ≤ ⊆ ( ℝ* × ℝ* )
4	2 3	ssexi	⊢ ≤ ∈ V