Definition df-nr 11008

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11073, 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 10817	. 2 class R
2		cnp 10811	. . . 4 class P
3	2, 2	cxp 5641	. . 3 class (P × P)
4		cer 10816	. . 3 class ~R
5	3, 4	cqs 8671	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1559	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  11016  addsrpr  11027  mulsrpr  11028  ltsrpr  11029  0nsr  11031  0r  11032  1sr  11033  m1r  11034  addclsr  11035  mulclsr  11036  addcomsr  11039  addasssr  11040  mulcomsr  11041  mulasssr  11042  distrsr  11043  ltsosr  11046  0idsr  11049  1idsr  11050  00sr  11051  ltasr  11052  recexsrlem  11055  mulgt0sr  11057  map2psrpr  11062  wuncn  11122