Definition df-1nq

Description: Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-2.2 of Gleason p. 117. (Contributed by NM, 29-Oct-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-1nq	$$⊢1_{𝑸}=⟨1_{𝑜},1_{𝑜}⟩$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1q	$$class{1}_{𝑸}$$
1		c1o	$$class{1}_{𝑜}$$
2	1 1	cop	$$class⟨1_{𝑜},1_{𝑜}⟩$$
3	0 2	wceq	$$wff{1}_{𝑸}=⟨1_{𝑜},1_{𝑜}⟩$$