Definition df-nr 11009

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

This definition is referenced by:  nrex1  11017  addsrpr  11028  mulsrpr  11029  ltsrpr  11030  0nsr  11032  0r  11033  1sr  11034  m1r  11035  addclsr  11036  mulclsr  11037  addcomsr  11040  addasssr  11041  mulcomsr  11042  mulasssr  11043  distrsr  11044  ltsosr  11047  0idsr  11050  1idsr  11051  00sr  11052  ltasr  11053  recexsrlem  11056  mulgt0sr  11058  map2psrpr  11063  wuncn  11123