Definition df-nr 10967

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11032, 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 10776	. 2 class R
2		cnp 10770	. . . 4 class P
3	2, 2	cxp 5622	. . 3 class (P × P)
4		cer 10775	. . 3 class ~R
5	3, 4	cqs 8634	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1541	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  10975  addsrpr  10986  mulsrpr  10987  ltsrpr  10988  0nsr  10990  0r  10991  1sr  10992  m1r  10993  addclsr  10994  mulclsr  10995  addcomsr  10998  addasssr  10999  mulcomsr  11000  mulasssr  11001  distrsr  11002  ltsosr  11005  0idsr  11008  1idsr  11009  00sr  11010  ltasr  11011  recexsrlem  11014  mulgt0sr  11016  map2psrpr  11021  wuncn  11081