enrex

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

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

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

Metamath Proof Explorer