Definition df-nr 8084

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers, 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.)

Assertion

Ref	Expression
df-nr	⊢ R = ((P × P) / ~R )

Detailed syntax breakdown of Definition df-nr

Step	Hyp	Ref	Expression
1		cnr 7654	. 2 class R
2		cnp 7648	. . . 4 class P
3	2, 2	cxp 4767	. . 3 class (P × P)
4		cer 7653	. . 3 class ~R
5	3, 4	cqs 6796	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1402	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  8102  mulsrpr  8103  ltsrprg  8104  gt0srpr  8105  0nsr  8106  0r  8107  1sr  8108  m1r  8109  addclsr  8110  mulclsr  8111  addcomsrg  8112  addasssrg  8113  mulcomsrg  8114  mulasssrg  8115  distrsrg  8116  lttrsr  8119  ltposr  8120  ltsosr  8121  0idsr  8124  1idsr  8125  00sr  8126  ltasrg  8127  recexgt0sr  8130  mulgt0sr  8135  aptisr  8136  mulextsr1  8138  archsr  8139  srpospr  8140  prsrcl  8141  ltpsrprg  8160  mappsrprg  8161  map2psrprg  8162  suplocsrlemb  8163  addvalex  8201  pitonnlem2  8204  pitore  8207  recnnre  8208  axcnex  8216