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	⊢ [Q] = ( ~Q ∩ ( ( N × N ) × Q ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cerq	⊢ [Q]
1		ceq	⊢ ~Q
2		cnpi	⊢ N
3	2 2	cxp	⊢ ( N × N )
4		cnq	⊢ Q
5	3 4	cxp	⊢ ( ( N × N ) × Q )
6	1 5	cin	⊢ ( ~Q ∩ ( ( N × N ) × Q ) )
7	0 6	wceq	⊢ [Q] = ( ~Q ∩ ( ( N × N ) × Q ) )