Definition df-nr 11036

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

This definition is referenced by:  nrex1  11044  addsrpr  11055  mulsrpr  11056  ltsrpr  11057  0nsr  11059  0r  11060  1sr  11061  m1r  11062  addclsr  11063  mulclsr  11064  addcomsr  11067  addasssr  11068  mulcomsr  11069  mulasssr  11070  distrsr  11071  ltsosr  11074  0idsr  11077  1idsr  11078  00sr  11079  ltasr  11080  recexsrlem  11083  mulgt0sr  11085  map2psrpr  11090  wuncn  11150