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

Definition df-nr 8891
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8698 . 2  class  R.
2 cnp 8690 . . . 4  class  P.
32, 2cxp 4835 . . 3  class  ( P. 
X.  P. )
4 cer 8697 . . 3  class  ~R
53, 4cqs 6863 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1649 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  8906  mulsrpr  8907  ltsrpr  8908  0nsr  8910  0r  8911  1sr  8912  m1r  8913  addclsr  8914  mulclsr  8915  addcomsr  8918  addasssr  8919  mulcomsr  8920  mulasssr  8921  distrsr  8922  ltsosr  8925  0idsr  8928  1idsr  8929  00sr  8930  ltasr  8931  recexsrlem  8934  mulgt0sr  8936  map2psrpr  8941  axcnex  8978  wuncn  9001
  Copyright terms: Public domain W3C validator