Definition df-nr 11051

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

This definition is referenced by:  nrex1  11059  addsrpr  11070  mulsrpr  11071  ltsrpr  11072  0nsr  11074  0r  11075  1sr  11076  m1r  11077  addclsr  11078  mulclsr  11079  addcomsr  11082  addasssr  11083  mulcomsr  11084  mulasssr  11085  distrsr  11086  ltsosr  11089  0idsr  11092  1idsr  11093  00sr  11094  ltasr  11095  recexsrlem  11098  mulgt0sr  11100  map2psrpr  11105  wuncn  11165