Definition df-nr 11037

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11102, 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 10846	. 2 class R
2		cnp 10840	. . . 4 class P
3	2, 2	cxp 5657	. . 3 class (P × P)
4		cer 10845	. . 3 class ~R
5	3, 4	cqs 8689	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1567	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  11045  addsrpr  11056  mulsrpr  11057  ltsrpr  11058  0nsr  11060  0r  11061  1sr  11062  m1r  11063  addclsr  11064  mulclsr  11065  addcomsr  11068  addasssr  11069  mulcomsr  11070  mulasssr  11071  distrsr  11072  ltsosr  11075  0idsr  11078  1idsr  11079  00sr  11080  ltasr  11081  recexsrlem  11084  mulgt0sr  11086  map2psrpr  11091  wuncn  11151