Definition df-nr 11125

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11190, 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 10934	. 2 class R
2		cnp 10928	. . . 4 class P
3	2, 2	cxp 5698	. . 3 class (P × P)
4		cer 10933	. . 3 class ~R
5	3, 4	cqs 8762	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1537	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  11133  addsrpr  11144  mulsrpr  11145  ltsrpr  11146  0nsr  11148  0r  11149  1sr  11150  m1r  11151  addclsr  11152  mulclsr  11153  addcomsr  11156  addasssr  11157  mulcomsr  11158  mulasssr  11159  distrsr  11160  ltsosr  11163  0idsr  11166  1idsr  11167  00sr  11168  ltasr  11169  recexsrlem  11172  mulgt0sr  11174  map2psrpr  11179  wuncn  11239