Definition df-nr 10805

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10870, 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 10614	. 2 class R
2		cnp 10608	. . . 4 class P
3	2, 2	cxp 5587	. . 3 class (P × P)
4		cer 10613	. . 3 class ~R
5	3, 4	cqs 8472	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1542	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  10813  addsrpr  10824  mulsrpr  10825  ltsrpr  10826  0nsr  10828  0r  10829  1sr  10830  m1r  10831  addclsr  10832  mulclsr  10833  addcomsr  10836  addasssr  10837  mulcomsr  10838  mulasssr  10839  distrsr  10840  ltsosr  10843  0idsr  10846  1idsr  10847  00sr  10848  ltasr  10849  recexsrlem  10852  mulgt0sr  10854  map2psrpr  10859  wuncn  10919