Definition df-erq 10913

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

Assertion

Ref	Expression
df-erq	⊢ [Q] = ( ~Q ∩ ((N × N) × Q))

Detailed syntax breakdown of Definition df-erq

Step	Hyp	Ref	Expression
1		cerq 10854	. 2 class [Q]
2		ceq 10851	. . 3 class ~Q
3		cnpi 10844	. . . . 5 class N
4	3, 3	cxp 5661	. . . 4 class (N × N)
5		cnq 10852	. . . 4 class Q
6	4, 5	cxp 5661	. . 3 class ((N × N) × Q)
7	2, 6	cin 3905	. 2 class ( ~Q ∩ ((N × N) × Q))
8	1, 7	wceq 1570	1 wff [Q] = ( ~Q ∩ ((N × N) × Q))

This definition is used by:  nqerf  10930  nqerrel  10932  nqerid  10933