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

Metamath Proof Explorer

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 ∈ ℂ ↔ A ∈ 𝑹 ∧ B ∈ 𝑹

Proof

Step Hyp Ref Expression
1 df-c ⊢ ℂ = 𝑹 × 𝑹
2 1 eleq2i ⊢ A B ∈ ℂ ↔ A B ∈ 𝑹 × 𝑹
3 opelxp ⊢ A B ∈ 𝑹 × 𝑹 ↔ A ∈ 𝑹 ∧ B ∈ 𝑹
4 2 3 bitri ⊢ A B ∈ ℂ ↔ A ∈ 𝑹 ∧ B ∈ 𝑹