0r

Description: The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	0r	$⊢ 0_{𝑹} \in 𝑹$

Step	Hyp	Ref	Expression
1		1pr	$⊢ 1_{𝑷} \in 𝑷$
2		opelxpi	$⊢ (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \to ⟨1_{𝑷}, 1_{𝑷}⟩ \in (𝑷 \times 𝑷)$
3	1 1 2	mp2an	$⊢ ⟨1_{𝑷}, 1_{𝑷}⟩ \in (𝑷 \times 𝑷)$
4		enrex	$⊢ ~_{𝑹} \in V$
5	4	ecelqsi	$⊢ ⟨1_{𝑷}, 1_{𝑷}⟩ \in (𝑷 \times 𝑷) \to [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
6	3 5	ax-mp	$⊢ [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
7		df-0r	$⊢ 0_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
8		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
9	6 7 8	3eltr4i	$⊢ 0_{𝑹} \in 𝑹$

Metamath Proof Explorer