Step |
Hyp |
Ref |
Expression |
1 |
|
relres |
|- Rel ( R |` A ) |
2 |
|
relopab |
|- Rel { <. x , y >. | ( x e. A /\ x R y ) } |
3 |
|
vex |
|- z e. _V |
4 |
|
vex |
|- w e. _V |
5 |
|
eleq1w |
|- ( x = z -> ( x e. A <-> z e. A ) ) |
6 |
|
breq1 |
|- ( x = z -> ( x R y <-> z R y ) ) |
7 |
5 6
|
anbi12d |
|- ( x = z -> ( ( x e. A /\ x R y ) <-> ( z e. A /\ z R y ) ) ) |
8 |
|
breq2 |
|- ( y = w -> ( z R y <-> z R w ) ) |
9 |
8
|
anbi2d |
|- ( y = w -> ( ( z e. A /\ z R y ) <-> ( z e. A /\ z R w ) ) ) |
10 |
3 4 7 9
|
opelopab |
|- ( <. z , w >. e. { <. x , y >. | ( x e. A /\ x R y ) } <-> ( z e. A /\ z R w ) ) |
11 |
4
|
brresi |
|- ( z ( R |` A ) w <-> ( z e. A /\ z R w ) ) |
12 |
|
df-br |
|- ( z ( R |` A ) w <-> <. z , w >. e. ( R |` A ) ) |
13 |
10 11 12
|
3bitr2ri |
|- ( <. z , w >. e. ( R |` A ) <-> <. z , w >. e. { <. x , y >. | ( x e. A /\ x R y ) } ) |
14 |
1 2 13
|
eqrelriiv |
|- ( R |` A ) = { <. x , y >. | ( x e. A /\ x R y ) } |