Step |
Hyp |
Ref |
Expression |
1 |
|
cbvmptv.1 |
|- ( x = y -> B = C ) |
2 |
|
eleq1w |
|- ( x = y -> ( x e. A <-> y e. A ) ) |
3 |
1
|
eqeq2d |
|- ( x = y -> ( z = B <-> z = C ) ) |
4 |
2 3
|
anbi12d |
|- ( x = y -> ( ( x e. A /\ z = B ) <-> ( y e. A /\ z = C ) ) ) |
5 |
4
|
cbvopab1v |
|- { <. x , z >. | ( x e. A /\ z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) } |
6 |
|
df-mpt |
|- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) } |
7 |
|
df-mpt |
|- ( y e. A |-> C ) = { <. y , z >. | ( y e. A /\ z = C ) } |
8 |
5 6 7
|
3eqtr4i |
|- ( x e. A |-> B ) = ( y e. A |-> C ) |