Definition df-nr 10969

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

This definition is referenced by:  nrex1  10977  addsrpr  10988  mulsrpr  10989  ltsrpr  10990  0nsr  10992  0r  10993  1sr  10994  m1r  10995  addclsr  10996  mulclsr  10997  addcomsr  11000  addasssr  11001  mulcomsr  11002  mulasssr  11003  distrsr  11004  ltsosr  11007  0idsr  11010  1idsr  11011  00sr  11012  ltasr  11013  recexsrlem  11016  mulgt0sr  11018  map2psrpr  11023  wuncn  11083