# Metamath Proof Explorer

## 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}⟩↔{A}{\cdot }_{𝑵}{D}={B}{\cdot }_{𝑵}{C}\right)$

### Proof

Step Hyp Ref Expression
1 df-enq ${⊢}{~}_{𝑸}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(𝑵×𝑵\right)\wedge {y}\in \left(𝑵×𝑵\right)\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\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}⟩↔{A}{\cdot }_{𝑵}{D}={B}{\cdot }_{𝑵}{C}\right)$