Definition df-nr 11134

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

This definition is used by:  nrex1  11142  addsrpr  11153  mulsrpr  11154  ltsrpr  11155  0nsr  11157  0r  11158  1sr  11159  m1r  11160  addclsr  11161  mulclsr  11162  addcomsr  11165  addasssr  11166  mulcomsr  11167  mulasssr  11168  distrsr  11169  ltsosr  11172  0idsr  11175  1idsr  11176  00sr  11177  ltasr  11178  recexsrlem  11181  mulgt0sr  11183  map2psrpr  11188  wuncn  11248