Definition df-nr 11065

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

This definition is used by:  nrex1  11073  addsrpr  11084  mulsrpr  11085  ltsrpr  11086  0nsr  11088  0r  11089  1sr  11090  m1r  11091  addclsr  11092  mulclsr  11093  addcomsr  11096  addasssr  11097  mulcomsr  11098  mulasssr  11099  distrsr  11100  ltsosr  11103  0idsr  11106  1idsr  11107  00sr  11108  ltasr  11109  recexsrlem  11112  mulgt0sr  11114  map2psrpr  11119  wuncn  11179