Theorem nrex1

Description: The class of signed reals is a set. Note that a shorter proof is possible using qsex (and not requiring enrer ), but it would add a dependency on ax-rep . (Contributed by Mario Carneiro, 17-Nov-2014) Extract proof from that of axcnex . (Revised by BJ, 4-Feb-2023) (New usage is discouraged.)

	Ref	Expression
Assertion	nrex1	$$⊢𝑹\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-nr	$$⊢𝑹=\left(𝑷\times 𝑷\right)/{~}_{𝑹}$$
2		npex	$$⊢𝑷\in \mathrm{V}$$
3	2 2	xpex	$$⊢𝑷\times 𝑷\in \mathrm{V}$$
4	3	pwex	$$⊢𝒫\left(𝑷\times 𝑷\right)\in \mathrm{V}$$
5		enrer	$$⊢{~}_{𝑹}\mathrm{Er}\left(𝑷\times 𝑷\right)$$
6	5	a1i	$$⊢\top \to {~}_{𝑹}\mathrm{Er}\left(𝑷\times 𝑷\right)$$
7	6	qsss	$$⊢\top \to \left(𝑷\times 𝑷\right)/{~}_{𝑹}\subseteq 𝒫\left(𝑷\times 𝑷\right)$$
8	7	mptru	$$⊢\left(𝑷\times 𝑷\right)/{~}_{𝑹}\subseteq 𝒫\left(𝑷\times 𝑷\right)$$
9	4 8	ssexi	$$⊢\left(𝑷\times 𝑷\right)/{~}_{𝑹}\in \mathrm{V}$$
10	1 9	eqeltri	$$⊢𝑹\in \mathrm{V}$$