Definition df-nr 10812

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10877, 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 10621	. 2 class R
2		cnp 10615	. . . 4 class P
3	2, 2	cxp 5587	. . 3 class (P × P)
4		cer 10620	. . 3 class ~R
5	3, 4	cqs 8497	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1539	1 wff R = ((P × P) / ~R )

This definition is referenced by:  nrex1  10820  addsrpr  10831  mulsrpr  10832  ltsrpr  10833  0nsr  10835  0r  10836  1sr  10837  m1r  10838  addclsr  10839  mulclsr  10840  addcomsr  10843  addasssr  10844  mulcomsr  10845  mulasssr  10846  distrsr  10847  ltsosr  10850  0idsr  10853  1idsr  10854  00sr  10855  ltasr  10856  recexsrlem  10859  mulgt0sr  10861  map2psrpr  10866  wuncn  10926