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 𝑹