Definition df-nr 11047

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

This definition is referenced by:  nrex1  11055  addsrpr  11066  mulsrpr  11067  ltsrpr  11068  0nsr  11070  0r  11071  1sr  11072  m1r  11073  addclsr  11074  mulclsr  11075  addcomsr  11078  addasssr  11079  mulcomsr  11080  mulasssr  11081  distrsr  11082  ltsosr  11085  0idsr  11088  1idsr  11089  00sr  11090  ltasr  11091  recexsrlem  11094  mulgt0sr  11096  map2psrpr  11101  wuncn  11161