Theorem enqbreq

Description: Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	enqbreq	$$⊢\left(\left(A\in 𝑵\wedge B\in 𝑵\right)\wedge \left(C\in 𝑵\wedge D\in 𝑵\right)\right)\to \left(⟨A,B⟩{~}_{𝑸}⟨C,D⟩\leftrightarrow A{\cdot }_{𝑵}D=B{\cdot }_{𝑵}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		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\}$$
2	1	ecopoveq	$$⊢\left(\left(A\in 𝑵\wedge B\in 𝑵\right)\wedge \left(C\in 𝑵\wedge D\in 𝑵\right)\right)\to \left(⟨A,B⟩{~}_{𝑸}⟨C,D⟩\leftrightarrow A{\cdot }_{𝑵}D=B{\cdot }_{𝑵}C\right)$$