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 ) |