Definition df-nr 11081

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11146, 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 10890	. 2 class R
2		cnp 10884	. . . 4 class P
3	2, 2	cxp 5676	. . 3 class (P × P)
4		cer 10889	. . 3 class ~R
5	3, 4	cqs 8724	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1533	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  11089  addsrpr  11100  mulsrpr  11101  ltsrpr  11102  0nsr  11104  0r  11105  1sr  11106  m1r  11107  addclsr  11108  mulclsr  11109  addcomsr  11112  addasssr  11113  mulcomsr  11114  mulasssr  11115  distrsr  11116  ltsosr  11119  0idsr  11122  1idsr  11123  00sr  11124  ltasr  11125  recexsrlem  11128  mulgt0sr  11130  map2psrpr  11135  wuncn  11195