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

Metamath Proof Explorer

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 , 0R >. e. RR <-> A e. R. )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  0R = 0R
2 df-r 
 |-  RR = ( R. X. { 0R } )
3 2 eleq2i 
 |-  ( <. A , 0R >. e. RR <-> <. A , 0R >. e. ( R. X. { 0R } ) )
4 opelxp 
 |-  ( <. A , 0R >. e. ( R. X. { 0R } ) <-> ( A e. R. /\ 0R e. { 0R } ) )
5 0r 
 |-  0R e. R.
6 5 elexi 
 |-  0R e. _V
7 6 elsn 
 |-  ( 0R e. { 0R } <-> 0R = 0R )
8 7 anbi2i 
 |-  ( ( A e. R. /\ 0R e. { 0R } ) <-> ( A e. R. /\ 0R = 0R ) )
9 3 4 8 3bitri 
 |-  ( <. A , 0R >. e. RR <-> ( A e. R. /\ 0R = 0R ) )
10 1 9 mpbiran2 
 |-  ( <. A , 0R >. e. RR <-> A e. R. )