Definition df-nr 11068

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

This definition is referenced by:  nrex1  11076  addsrpr  11087  mulsrpr  11088  ltsrpr  11089  0nsr  11091  0r  11092  1sr  11093  m1r  11094  addclsr  11095  mulclsr  11096  addcomsr  11099  addasssr  11100  mulcomsr  11101  mulasssr  11102  distrsr  11103  ltsosr  11106  0idsr  11109  1idsr  11110  00sr  11111  ltasr  11112  recexsrlem  11115  mulgt0sr  11117  map2psrpr  11122  wuncn  11182