This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑸$

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 𝑸$