Definition df-nr 9878

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9687	. 2 class R
2		cnp 9681	. . . 4 class P
3	2, 2	cxp 5112	. . 3 class (P × P)
4		cer 9686	. . 3 class ~R
5	3, 4	cqs 7741	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1483	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  9896  mulsrpr  9897  ltsrpr  9898  0nsr  9900  0r  9901  1sr  9902  m1r  9903  addclsr  9904  mulclsr  9905  addcomsr  9908  addasssr  9909  mulcomsr  9910  mulasssr  9911  distrsr  9912  ltsosr  9915  0idsr  9918  1idsr  9919  00sr  9920  ltasr  9921  recexsrlem  9924  mulgt0sr  9926  map2psrpr  9931  axcnex  9968  wuncn  9991