Theorem leex

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

	Ref	Expression
Assertion	leex	$$⊢\le \in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
2	1 1	xpex	$$⊢{ℝ}^{*}\times {ℝ}^{*}\in \mathrm{V}$$
3		lerelxr	$$⊢\le \subseteq {ℝ}^{*}\times {ℝ}^{*}$$
4	2 3	ssexi	$$⊢\le \in \mathrm{V}$$