Definition df-nr 10743

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10808, 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 10552	. 2 class R
2		cnp 10546	. . . 4 class P
3	2, 2	cxp 5578	. . 3 class (P × P)
4		cer 10551	. . 3 class ~R
5	3, 4	cqs 8455	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1539	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  10751  addsrpr  10762  mulsrpr  10763  ltsrpr  10764  0nsr  10766  0r  10767  1sr  10768  m1r  10769  addclsr  10770  mulclsr  10771  addcomsr  10774  addasssr  10775  mulcomsr  10776  mulasssr  10777  distrsr  10778  ltsosr  10781  0idsr  10784  1idsr  10785  00sr  10786  ltasr  10787  recexsrlem  10790  mulgt0sr  10792  map2psrpr  10797  wuncn  10857