Definition df-nr 7794

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 7364	. 2 class R
2		cnp 7358	. . . 4 class P
3	2, 2	cxp 4661	. . 3 class (P × P)
4		cer 7363	. . 3 class ~R
5	3, 4	cqs 6591	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1364	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7812  mulsrpr  7813  ltsrprg  7814  gt0srpr  7815  0nsr  7816  0r  7817  1sr  7818  m1r  7819  addclsr  7820  mulclsr  7821  addcomsrg  7822  addasssrg  7823  mulcomsrg  7824  mulasssrg  7825  distrsrg  7826  lttrsr  7829  ltposr  7830  ltsosr  7831  0idsr  7834  1idsr  7835  00sr  7836  ltasrg  7837  recexgt0sr  7840  mulgt0sr  7845  aptisr  7846  mulextsr1  7848  archsr  7849  srpospr  7850  prsrcl  7851  ltpsrprg  7870  mappsrprg  7871  map2psrprg  7872  suplocsrlemb  7873  addvalex  7911  pitonnlem2  7914  pitore  7917  recnnre  7918  axcnex  7926