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	⊢ 1Q = ⟨ 1o , 1o ⟩

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1q	⊢ 1Q
1		c1o	⊢ 1o
2	1 1	cop	⊢ ⟨ 1o , 1o ⟩
3	0 2	wceq	⊢ 1Q = ⟨ 1o , 1o ⟩