Definition df-nr 11148

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

This definition is used by:  nrex1  11156  addsrpr  11167  mulsrpr  11168  ltsrpr  11169  0nsr  11171  0r  11172  1sr  11173  m1r  11174  addclsr  11175  mulclsr  11176  addcomsr  11179  addasssr  11180  mulcomsr  11181  mulasssr  11182  distrsr  11183  ltsosr  11186  0idsr  11189  1idsr  11190  00sr  11191  ltasr  11192  recexsrlem  11195  mulgt0sr  11197  map2psrpr  11202  wuncn  11262