Step |
Hyp |
Ref |
Expression |
1 |
|
opeq2 |
|- ( y = w -> <. x , y >. = <. x , w >. ) |
2 |
1
|
eleq1d |
|- ( y = w -> ( <. x , y >. e. B <-> <. x , w >. e. B ) ) |
3 |
2
|
exbidv |
|- ( y = w -> ( E. x <. x , y >. e. B <-> E. x <. x , w >. e. B ) ) |
4 |
|
opeq2 |
|- ( w = A -> <. x , w >. = <. x , A >. ) |
5 |
4
|
eleq1d |
|- ( w = A -> ( <. x , w >. e. B <-> <. x , A >. e. B ) ) |
6 |
5
|
exbidv |
|- ( w = A -> ( E. x <. x , w >. e. B <-> E. x <. x , A >. e. B ) ) |
7 |
|
dfrn3 |
|- ran B = { y | E. x <. x , y >. e. B } |
8 |
3 6 7
|
elab2gw |
|- ( A e. V -> ( A e. ran B <-> E. x <. x , A >. e. B ) ) |