Definition df-nr 11096

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

This definition is referenced by:  nrex1  11104  addsrpr  11115  mulsrpr  11116  ltsrpr  11117  0nsr  11119  0r  11120  1sr  11121  m1r  11122  addclsr  11123  mulclsr  11124  addcomsr  11127  addasssr  11128  mulcomsr  11129  mulasssr  11130  distrsr  11131  ltsosr  11134  0idsr  11137  1idsr  11138  00sr  11139  ltasr  11140  recexsrlem  11143  mulgt0sr  11145  map2psrpr  11150  wuncn  11210