Definition df-nr 10985

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

This definition is referenced by:  nrex1  10993  addsrpr  11004  mulsrpr  11005  ltsrpr  11006  0nsr  11008  0r  11009  1sr  11010  m1r  11011  addclsr  11012  mulclsr  11013  addcomsr  11016  addasssr  11017  mulcomsr  11018  mulasssr  11019  distrsr  11020  ltsosr  11023  0idsr  11026  1idsr  11027  00sr  11028  ltasr  11029  recexsrlem  11032  mulgt0sr  11034  map2psrpr  11039  wuncn  11099