Definition df-erq 9735

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 9752. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
df-erq	|- /Q = ( ~Q i^i ( ( N. X. N. ) X. Q. ) )

Detailed syntax breakdown of Definition df-erq

Step	Hyp	Ref	Expression
1		cerq 9676	. 2 class /Q
2		ceq 9673	. . 3 class ~Q
3		cnpi 9666	. . . . 5 class N.
4	3, 3	cxp 5112	. . . 4 class ( N. X. N. )
5		cnq 9674	. . . 4 class Q.
6	4, 5	cxp 5112	. . 3 class ( ( N. X. N. ) X. Q. )
7	2, 6	cin 3573	. 2 class ( ~Q i^i ( ( N. X. N. ) X. Q. ) )
8	1, 7	wceq 1483	1 wff /Q = ( ~Q i^i ( ( N. X. N. ) X. Q. ) )

This definition is referenced by:  nqerf  9752  nqerrel  9754  nqerid  9755