Definition df-nr 9757

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9821, 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 9566	. 2 class R
2		cnp 9560	. . . 4 class P
3	2, 2	cxp 5036	. . 3 class (P × P)
4		cer 9565	. . 3 class ~R
5	3, 4	cqs 7628	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1475	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  9775  mulsrpr  9776  ltsrpr  9777  0nsr  9779  0r  9780  1sr  9781  m1r  9782  addclsr  9783  mulclsr  9784  addcomsr  9787  addasssr  9788  mulcomsr  9789  mulasssr  9790  distrsr  9791  ltsosr  9794  0idsr  9797  1idsr  9798  00sr  9799  ltasr  9800  recexsrlem  9803  mulgt0sr  9805  map2psrpr  9810  axcnex  9847  wuncn  9870