Definition df-erq

Description: Define a convenience function that "reduces" a fraction to lowest terms. Note that in this form, it is not obviously a function; we prove this in nqerf . (Contributed by NM, 27-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-erq	$$⊢{/}_{𝑸}={~}_{𝑸}\cap \left(\left(𝑵\times 𝑵\right)\times 𝑸\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cerq	$$class{/}_{𝑸}$$
1		ceq	$$class{~}_{𝑸}$$
2		cnpi	$$class𝑵$$
3	2 2	cxp	$$class\left(𝑵\times 𝑵\right)$$
4		cnq	$$class𝑸$$
5	3 4	cxp	$$class\left(\left(𝑵\times 𝑵\right)\times 𝑸\right)$$
6	1 5	cin	$$class\left({~}_{𝑸}\cap \left(\left(𝑵\times 𝑵\right)\times 𝑸\right)\right)$$
7	0 6	wceq	$$wff{/}_{𝑸}={~}_{𝑸}\cap \left(\left(𝑵\times 𝑵\right)\times 𝑸\right)$$