Definition df-nr 10950

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11015, 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 10759	. 2 class R
2		cnp 10753	. . . 4 class P
3	2, 2	cxp 5617	. . 3 class (P × P)
4		cer 10758	. . 3 class ~R
5	3, 4	cqs 8624	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1540	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  10958  addsrpr  10969  mulsrpr  10970  ltsrpr  10971  0nsr  10973  0r  10974  1sr  10975  m1r  10976  addclsr  10977  mulclsr  10978  addcomsr  10981  addasssr  10982  mulcomsr  10983  mulasssr  10984  distrsr  10985  ltsosr  10988  0idsr  10991  1idsr  10992  00sr  10993  ltasr  10994  recexsrlem  10997  mulgt0sr  10999  map2psrpr  11004  wuncn  11064