Definition df-nr 10481

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10546, 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 10290	. 2 class R
2		cnp 10284	. . . 4 class P
3	2, 2	cxp 5556	. . 3 class (P × P)
4		cer 10289	. . 3 class ~R
5	3, 4	cqs 8291	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1536	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  10489  addsrpr  10500  mulsrpr  10501  ltsrpr  10502  0nsr  10504  0r  10505  1sr  10506  m1r  10507  addclsr  10508  mulclsr  10509  addcomsr  10512  addasssr  10513  mulcomsr  10514  mulasssr  10515  distrsr  10516  ltsosr  10519  0idsr  10522  1idsr  10523  00sr  10524  ltasr  10525  recexsrlem  10528  mulgt0sr  10530  map2psrpr  10535  wuncn  10595