Definition df-nr 10958

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

This definition is referenced by:  nrex1  10966  addsrpr  10977  mulsrpr  10978  ltsrpr  10979  0nsr  10981  0r  10982  1sr  10983  m1r  10984  addclsr  10985  mulclsr  10986  addcomsr  10989  addasssr  10990  mulcomsr  10991  mulasssr  10992  distrsr  10993  ltsosr  10996  0idsr  10999  1idsr  11000  00sr  11001  ltasr  11002  recexsrlem  11005  mulgt0sr  11007  map2psrpr  11012  wuncn  11072