Definition df-nr 10942

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11007, 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 10751	. 2 class R
2		cnp 10745	. . . 4 class P
3	2, 2	cxp 5609	. . 3 class (P × P)
4		cer 10750	. . 3 class ~R
5	3, 4	cqs 8616	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1541	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  10950  addsrpr  10961  mulsrpr  10962  ltsrpr  10963  0nsr  10965  0r  10966  1sr  10967  m1r  10968  addclsr  10969  mulclsr  10970  addcomsr  10973  addasssr  10974  mulcomsr  10975  mulasssr  10976  distrsr  10977  ltsosr  10980  0idsr  10983  1idsr  10984  00sr  10985  ltasr  10986  recexsrlem  10989  mulgt0sr  10991  map2psrpr  10996  wuncn  11056