Theorem 1nq

Description: The positive fraction 'one'. (Contributed by NM, 29-Oct-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	1nq	$$⊢1_{𝑸}\in 𝑸$$

Proof

Step	Hyp	Ref	Expression
1		df-1nq	$$⊢1_{𝑸}=⟨1_{𝑜},1_{𝑜}⟩$$
2		1pi	$$⊢1_{𝑜}\in 𝑵$$
3		pinq	$$⊢1_{𝑜}\in 𝑵\to ⟨1_{𝑜},1_{𝑜}⟩\in 𝑸$$
4	2 3	ax-mp	$$⊢⟨1_{𝑜},1_{𝑜}⟩\in 𝑸$$
5	1 4	eqeltri	$$⊢1_{𝑸}\in 𝑸$$