Definition df-nr 11056

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11121, 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 10865	. 2 class R
2		cnp 10859	. . . 4 class P
3	2, 2	cxp 5661	. . 3 class (P × P)
4		cer 10864	. . 3 class ~R
5	3, 4	cqs 8699	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1570	1 wff R = ((P × P) / ~R )

This definition is used by:  nrex1  11064  addsrpr  11075  mulsrpr  11076  ltsrpr  11077  0nsr  11079  0r  11080  1sr  11081  m1r  11082  addclsr  11083  mulclsr  11084  addcomsr  11087  addasssr  11088  mulcomsr  11089  mulasssr  11090  distrsr  11091  ltsosr  11094  0idsr  11097  1idsr  11098  00sr  11099  ltasr  11100  recexsrlem  11103  mulgt0sr  11105  map2psrpr  11110  wuncn  11170