Definition df-nr 10979

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

This definition is referenced by:  nrex1  10987  addsrpr  10998  mulsrpr  10999  ltsrpr  11000  0nsr  11002  0r  11003  1sr  11004  m1r  11005  addclsr  11006  mulclsr  11007  addcomsr  11010  addasssr  11011  mulcomsr  11012  mulasssr  11013  distrsr  11014  ltsosr  11017  0idsr  11020  1idsr  11021  00sr  11022  ltasr  11023  recexsrlem  11026  mulgt0sr  11028  map2psrpr  11033  wuncn  11093