Theorem enrex

Description: The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	enrex	$$⊢{~}_{𝑹}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		npex	$$⊢𝑷\in \mathrm{V}$$
2	1 1	xpex	$$⊢𝑷\times 𝑷\in \mathrm{V}$$
3	2 2	xpex	$$⊢\left(𝑷\times 𝑷\right)\times \left(𝑷\times 𝑷\right)\in \mathrm{V}$$
4		df-enr	$$⊢{~}_{𝑹}=\left\{⟨x,y⟩|\left(\left(x\in \left(𝑷\times 𝑷\right)\wedge y\in \left(𝑷\times 𝑷\right)\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=⟨z,w⟩\wedge y=⟨v,u⟩\right)\wedge z{+}_{𝑷}u=w{+}_{𝑷}v\right)\right)\right\}$$
5		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in \left(𝑷\times 𝑷\right)\wedge y\in \left(𝑷\times 𝑷\right)\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=⟨z,w⟩\wedge y=⟨v,u⟩\right)\wedge z{+}_{𝑷}u=w{+}_{𝑷}v\right)\right)\right\}\subseteq \left(𝑷\times 𝑷\right)\times \left(𝑷\times 𝑷\right)$$
6	4 5	eqsstri	$$⊢{~}_{𝑹}\subseteq \left(𝑷\times 𝑷\right)\times \left(𝑷\times 𝑷\right)$$
7	3 6	ssexi	$$⊢{~}_{𝑹}\in \mathrm{V}$$