Definition df-nr 10670

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10735, 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 10479	. 2 class R
2		cnp 10473	. . . 4 class P
3	2, 2	cxp 5549	. . 3 class (P × P)
4		cer 10478	. . 3 class ~R
5	3, 4	cqs 8390	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1543	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  10678  addsrpr  10689  mulsrpr  10690  ltsrpr  10691  0nsr  10693  0r  10694  1sr  10695  m1r  10696  addclsr  10697  mulclsr  10698  addcomsr  10701  addasssr  10702  mulcomsr  10703  mulasssr  10704  distrsr  10705  ltsosr  10708  0idsr  10711  1idsr  10712  00sr  10713  ltasr  10714  recexsrlem  10717  mulgt0sr  10719  map2psrpr  10724  wuncn  10784