Definition df-nr 11180

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11245, 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 10989	. 2 class R
2		cnp 10983	. . . 4 class P
3	2, 2	cxp 5656	. . 3 class (P × P)
4		cer 10988	. . 3 class ~R
5	3, 4	cqs 8754	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1570	1 wff R = ((P × P) / ~R )

This definition is used by:  nrex1  11188  addsrpr  11199  mulsrpr  11200  ltsrpr  11201  0nsr  11203  0r  11204  1sr  11205  m1r  11206  addclsr  11207  mulclsr  11208  addcomsr  11211  addasssr  11212  mulcomsr  11213  mulasssr  11214  distrsr  11215  ltsosr  11218  0idsr  11221  1idsr  11222  00sr  11223  ltasr  11224  recexsrlem  11227  mulgt0sr  11229  map2psrpr  11234  wuncn  11294