Theorem enqex

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

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

Proof

Step	Hyp	Ref	Expression
1		niex	$$⊢𝑵\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-enq	$$⊢{~}_{𝑸}=\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{\cdot }_{𝑵}u=w{\cdot }_{𝑵}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{\cdot }_{𝑵}u=w{\cdot }_{𝑵}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}$$