Definition df-nr 10160

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10224, 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 × P) / ~R )

Detailed syntax breakdown of Definition df-nr

Step	Hyp	Ref	Expression
1		cnr 9969	. 2 class R
2		cnp 9963	. . . 4 class P
3	2, 2	cxp 5306	. . 3 class (P × P)
4		cer 9968	. . 3 class ~R
5	3, 4	cqs 7975	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1637	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  10178  mulsrpr  10179  ltsrpr  10180  0nsr  10182  0r  10183  1sr  10184  m1r  10185  addclsr  10186  mulclsr  10187  addcomsr  10190  addasssr  10191  mulcomsr  10192  mulasssr  10193  distrsr  10194  ltsosr  10197  0idsr  10200  1idsr  10201  00sr  10202  ltasr  10203  recexsrlem  10206  mulgt0sr  10208  map2psrpr  10213  axcnex  10250  wuncn  10273