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

Metamath Proof Explorer

Theorem elreal

Description: Membership in class of real numbers. (Contributed by NM, 31-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion elreal 
|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )

Proof

Step Hyp Ref Expression
1 df-r 
 |-  RR = ( R. X. { 0R } )
2 1 eleq2i 
 |-  ( A e. RR <-> A e. ( R. X. { 0R } ) )
3 elxp2 
 |-  ( A e. ( R. X. { 0R } ) <-> E. x e. R. E. y e. { 0R } A = <. x , y >. )
4 0r 
 |-  0R e. R.
5 4 elexi 
 |-  0R e. _V
6 opeq2 
 |-  ( y = 0R -> <. x , y >. = <. x , 0R >. )
7 6 eqeq2d 
 |-  ( y = 0R -> ( A = <. x , y >. <-> A = <. x , 0R >. ) )
8 5 7 rexsn 
 |-  ( E. y e. { 0R } A = <. x , y >. <-> A = <. x , 0R >. )
9 eqcom 
 |-  ( A = <. x , 0R >. <-> <. x , 0R >. = A )
10 8 9 bitri 
 |-  ( E. y e. { 0R } A = <. x , y >. <-> <. x , 0R >. = A )
11 10 rexbii 
 |-  ( E. x e. R. E. y e. { 0R } A = <. x , y >. <-> E. x e. R. <. x , 0R >. = A )
12 3 11 bitri 
 |-  ( A e. ( R. X. { 0R } ) <-> E. x e. R. <. x , 0R >. = A )
13 2 12 bitri 
 |-  ( A e. RR <-> E. x e. R. <. x , 0R >. = A )