Definition df-nr 7370

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 6953	. 2 class R
2		cnp 6947	. . . 4 class P
3	2, 2	cxp 4465	. . 3 class (P × P)
4		cer 6952	. . 3 class ~R
5	3, 4	cqs 6331	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1296	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7388  mulsrpr  7389  ltsrprg  7390  gt0srpr  7391  0nsr  7392  0r  7393  1sr  7394  m1r  7395  addclsr  7396  mulclsr  7397  addcomsrg  7398  addasssrg  7399  mulcomsrg  7400  mulasssrg  7401  distrsrg  7402  lttrsr  7405  ltposr  7406  ltsosr  7407  0idsr  7410  1idsr  7411  00sr  7412  ltasrg  7413  recexgt0sr  7416  mulgt0sr  7420  aptisr  7421  mulextsr1  7423  archsr  7424  srpospr  7425  prsrcl  7426  addvalex  7478  pitonnlem2  7481  pitore  7484  recnnre  7485  axcnex  7493