Definition df-nr 10324

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10389, 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 10133	. 2 class R
2		cnp 10127	. . . 4 class P
3	2, 2	cxp 5441	. . 3 class (P × P)
4		cer 10132	. . 3 class ~R
5	3, 4	cqs 8138	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1522	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  10332  addsrpr  10343  mulsrpr  10344  ltsrpr  10345  0nsr  10347  0r  10348  1sr  10349  m1r  10350  addclsr  10351  mulclsr  10352  addcomsr  10355  addasssr  10356  mulcomsr  10357  mulasssr  10358  distrsr  10359  ltsosr  10362  0idsr  10365  1idsr  10366  00sr  10367  ltasr  10368  recexsrlem  10371  mulgt0sr  10373  map2psrpr  10378  wuncn  10438