Theorem opelcn

Description: Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	opelcn	$$⊢⟨A,B⟩\in ℂ\leftrightarrow \left(A\in 𝑹\wedge B\in 𝑹\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-c	$$⊢ℂ=𝑹\times 𝑹$$
2	1	eleq2i	$$⊢⟨A,B⟩\in ℂ\leftrightarrow ⟨A,B⟩\in \left(𝑹\times 𝑹\right)$$
3		opelxp	$$⊢⟨A,B⟩\in \left(𝑹\times 𝑹\right)\leftrightarrow \left(A\in 𝑹\wedge B\in 𝑹\right)$$
4	2 3	bitri	$$⊢⟨A,B⟩\in ℂ\leftrightarrow \left(A\in 𝑹\wedge B\in 𝑹\right)$$