Definition df-nr 7910

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 7480	. 2 class R
2		cnp 7474	. . . 4 class P
3	2, 2	cxp 4716	. . 3 class (P × P)
4		cer 7479	. . 3 class ~R
5	3, 4	cqs 6677	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1395	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7928  mulsrpr  7929  ltsrprg  7930  gt0srpr  7931  0nsr  7932  0r  7933  1sr  7934  m1r  7935  addclsr  7936  mulclsr  7937  addcomsrg  7938  addasssrg  7939  mulcomsrg  7940  mulasssrg  7941  distrsrg  7942  lttrsr  7945  ltposr  7946  ltsosr  7947  0idsr  7950  1idsr  7951  00sr  7952  ltasrg  7953  recexgt0sr  7956  mulgt0sr  7961  aptisr  7962  mulextsr1  7964  archsr  7965  srpospr  7966  prsrcl  7967  ltpsrprg  7986  mappsrprg  7987  map2psrprg  7988  suplocsrlemb  7989  addvalex  8027  pitonnlem2  8030  pitore  8033  recnnre  8034  axcnex  8042