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

Definition df-nr 8698
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8759, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)
Assertion
Ref Expression
df-nr  |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )

Detailed syntax breakdown of Definition df-nr
StepHypRef Expression
1 cnr 8505 . 2  class  R.
2 cnp 8497 . . . 4  class  P.
32, 2cxp 4703 . . 3  class  ( P. 
X.  P. )
4 cer 8504 . . 3  class  ~R
53, 4cqs 6675 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1632 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  8713  mulsrpr  8714  ltsrpr  8715  0nsr  8717  0r  8718  1sr  8719  m1r  8720  addclsr  8721  mulclsr  8722  addcomsr  8725  addasssr  8726  mulcomsr  8727  mulasssr  8728  distrsr  8729  ltsosr  8732  0idsr  8735  1idsr  8736  00sr  8737  ltasr  8738  recexsrlem  8741  mulgt0sr  8743  map2psrpr  8748  axcnex  8785  wuncn  8808
  Copyright terms: Public domain W3C validator