Definition df-nr 11016

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11081, 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 10825	. 2 class R
2		cnp 10819	. . . 4 class P
3	2, 2	cxp 5639	. . 3 class (P × P)
4		cer 10824	. . 3 class ~R
5	3, 4	cqs 8673	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1540	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  11024  addsrpr  11035  mulsrpr  11036  ltsrpr  11037  0nsr  11039  0r  11040  1sr  11041  m1r  11042  addclsr  11043  mulclsr  11044  addcomsr  11047  addasssr  11048  mulcomsr  11049  mulasssr  11050  distrsr  11051  ltsosr  11054  0idsr  11057  1idsr  11058  00sr  11059  ltasr  11060  recexsrlem  11063  mulgt0sr  11065  map2psrpr  11070  wuncn  11130