Theorem opelreal

Description: Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	opelreal	$$⊢⟨A,0_{𝑹}⟩\in ℝ\leftrightarrow A\in 𝑹$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢0_{𝑹}=0_{𝑹}$$
2		df-r	$$⊢ℝ=𝑹\times \left\{0_{𝑹}\right\}$$
3	2	eleq2i	$$⊢⟨A,0_{𝑹}⟩\in ℝ\leftrightarrow ⟨A,0_{𝑹}⟩\in \left(𝑹\times \left\{0_{𝑹}\right\}\right)$$
4		opelxp	$$⊢⟨A,0_{𝑹}⟩\in \left(𝑹\times \left\{0_{𝑹}\right\}\right)\leftrightarrow \left(A\in 𝑹\wedge 0_{𝑹}\in \left\{0_{𝑹}\right\}\right)$$
5		0r	$$⊢0_{𝑹}\in 𝑹$$
6	5	elexi	$$⊢0_{𝑹}\in \mathrm{V}$$
7	6	elsn	$$⊢0_{𝑹}\in \left\{0_{𝑹}\right\}\leftrightarrow 0_{𝑹}=0_{𝑹}$$
8	7	anbi2i	$$⊢\left(A\in 𝑹\wedge 0_{𝑹}\in \left\{0_{𝑹}\right\}\right)\leftrightarrow \left(A\in 𝑹\wedge 0_{𝑹}=0_{𝑹}\right)$$
9	3 4 8	3bitri	$$⊢⟨A,0_{𝑹}⟩\in ℝ\leftrightarrow \left(A\in 𝑹\wedge 0_{𝑹}=0_{𝑹}\right)$$
10	1 9	mpbiran2	$$⊢⟨A,0_{𝑹}⟩\in ℝ\leftrightarrow A\in 𝑹$$