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 >. e. CC <-> ( A e. R. /\ B e. R. ) )

Proof

Step Hyp Ref Expression
1 df-c 
 |-  CC = ( R. X. R. )
2 1 eleq2i 
 |-  ( <. A , B >. e. CC <-> <. A , B >. e. ( R. X. R. ) )
3 opelxp 
 |-  ( <. A , B >. e. ( R. X. R. ) <-> ( A e. R. /\ B e. R. ) )
4 2 3 bitri 
 |-  ( <. A , B >. e. CC <-> ( A e. R. /\ B e. R. ) )