enqex

Description: The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	enqex	$⊢ ~_{𝑸} \in V$

Step	Hyp	Ref	Expression
1		niex	$⊢ 𝑵 \in V$
2	1 1	xpex	$⊢ 𝑵 \times 𝑵 \in V$
3	2 2	xpex	$⊢ (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) \in V$
4		df-enq	$⊢ ~_{𝑸} = \{⟨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 \cdot_{𝑵} u = w \cdot_{𝑵} 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 \cdot_{𝑵} u = w \cdot_{𝑵} v))\} \subseteq (𝑵 \times 𝑵) \times (𝑵 \times 𝑵)$
6	4 5	eqsstri	$⊢ ~_{𝑸} \subseteq (𝑵 \times 𝑵) \times (𝑵 \times 𝑵)$
7	3 6	ssexi	$⊢ ~_{𝑸} \in V$

Metamath Proof Explorer