Definition df-nr 7937

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers, 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.)

Assertion

Ref	Expression
df-nr	⊢ R = ((P × P) / ~R )

Detailed syntax breakdown of Definition df-nr

Step	Hyp	Ref	Expression
1		cnr 7507	. 2 class R
2		cnp 7501	. . . 4 class P
3	2, 2	cxp 4721	. . 3 class (P × P)
4		cer 7506	. . 3 class ~R
5	3, 4	cqs 6696	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1395	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7955  mulsrpr  7956  ltsrprg  7957  gt0srpr  7958  0nsr  7959  0r  7960  1sr  7961  m1r  7962  addclsr  7963  mulclsr  7964  addcomsrg  7965  addasssrg  7966  mulcomsrg  7967  mulasssrg  7968  distrsrg  7969  lttrsr  7972  ltposr  7973  ltsosr  7974  0idsr  7977  1idsr  7978  00sr  7979  ltasrg  7980  recexgt0sr  7983  mulgt0sr  7988  aptisr  7989  mulextsr1  7991  archsr  7992  srpospr  7993  prsrcl  7994  ltpsrprg  8013  mappsrprg  8014  map2psrprg  8015  suplocsrlemb  8016  addvalex  8054  pitonnlem2  8057  pitore  8060  recnnre  8061  axcnex  8069