Theorem elreal

Description: Membership in class of real numbers. (Contributed by NM, 31-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	elreal	$$⊢A\in ℝ\leftrightarrow \exists x\in 𝑹⟨x,0_{𝑹}⟩=A$$

Proof

Step	Hyp	Ref	Expression
1		df-r	$$⊢ℝ=𝑹\times \left\{0_{𝑹}\right\}$$
2	1	eleq2i	$$⊢A\in ℝ\leftrightarrow A\in \left(𝑹\times \left\{0_{𝑹}\right\}\right)$$
3		elxp2	$$⊢A\in \left(𝑹\times \left\{0_{𝑹}\right\}\right)\leftrightarrow \exists x\in 𝑹\exists y\in \left\{0_{𝑹}\right\}A=⟨x,y⟩$$
4		0r	$$⊢0_{𝑹}\in 𝑹$$
5	4	elexi	$$⊢0_{𝑹}\in \mathrm{V}$$
6		opeq2	$$⊢y=0_{𝑹}\to ⟨x,y⟩=⟨x,0_{𝑹}⟩$$
7	6	eqeq2d	$$⊢y=0_{𝑹}\to \left(A=⟨x,y⟩\leftrightarrow A=⟨x,0_{𝑹}⟩\right)$$
8	5 7	rexsn	$$⊢\exists y\in \left\{0_{𝑹}\right\}A=⟨x,y⟩\leftrightarrow A=⟨x,0_{𝑹}⟩$$
9		eqcom	$$⊢A=⟨x,0_{𝑹}⟩\leftrightarrow ⟨x,0_{𝑹}⟩=A$$
10	8 9	bitri	$$⊢\exists y\in \left\{0_{𝑹}\right\}A=⟨x,y⟩\leftrightarrow ⟨x,0_{𝑹}⟩=A$$
11	10	rexbii	$$⊢\exists x\in 𝑹\exists y\in \left\{0_{𝑹}\right\}A=⟨x,y⟩\leftrightarrow \exists x\in 𝑹⟨x,0_{𝑹}⟩=A$$
12	3 11	bitri	$$⊢A\in \left(𝑹\times \left\{0_{𝑹}\right\}\right)\leftrightarrow \exists x\in 𝑹⟨x,0_{𝑹}⟩=A$$
13	2 12	bitri	$$⊢A\in ℝ\leftrightarrow \exists x\in 𝑹⟨x,0_{𝑹}⟩=A$$