Definition df-nr 10970

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

This definition is referenced by:  nrex1  10978  addsrpr  10989  mulsrpr  10990  ltsrpr  10991  0nsr  10993  0r  10994  1sr  10995  m1r  10996  addclsr  10997  mulclsr  10998  addcomsr  11001  addasssr  11002  mulcomsr  11003  mulasssr  11004  distrsr  11005  ltsosr  11008  0idsr  11011  1idsr  11012  00sr  11013  ltasr  11014  recexsrlem  11017  mulgt0sr  11019  map2psrpr  11024  wuncn  11084