MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-erq Unicode version

Definition df-erq 8537
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 8554. (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
StepHypRef Expression
1 cerq 8476 . 2  class  /Q
2 ceq 8473 . . 3  class  ~Q
3 cnpi 8466 . . . . 5  class  N.
43, 3cxp 4687 . . . 4  class  ( N. 
X.  N. )
5 cnq 8474 . . . 4  class  Q.
64, 5cxp 4687 . . 3  class  ( ( N.  X.  N. )  X.  Q. )
72, 6cin 3151 . 2  class  (  ~Q  i^i  ( ( N.  X.  N. )  X.  Q. )
)
81, 7wceq 1623 1  wff  /Q  =  (  ~Q  i^i  ( ( N.  X.  N. )  X.  Q. ) )
Colors of variables: wff set class
This definition is referenced by:  nqerf  8554  nqerrel  8556  nqerid  8557
  Copyright terms: Public domain W3C validator