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 )