Step |
Hyp |
Ref |
Expression |
1 |
|
raleq |
|- ( B = C -> ( A. y e. B -. x R y <-> A. y e. C -. x R y ) ) |
2 |
|
rexeq |
|- ( B = C -> ( E. z e. B y R z <-> E. z e. C y R z ) ) |
3 |
2
|
imbi2d |
|- ( B = C -> ( ( y R x -> E. z e. B y R z ) <-> ( y R x -> E. z e. C y R z ) ) ) |
4 |
3
|
ralbidv |
|- ( B = C -> ( A. y e. A ( y R x -> E. z e. B y R z ) <-> A. y e. A ( y R x -> E. z e. C y R z ) ) ) |
5 |
1 4
|
anbi12d |
|- ( B = C -> ( ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) <-> ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) ) ) |
6 |
5
|
rabbidv |
|- ( B = C -> { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } = { x e. A | ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) } ) |
7 |
6
|
unieqd |
|- ( B = C -> U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } = U. { x e. A | ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) } ) |
8 |
|
df-sup |
|- sup ( B , A , R ) = U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } |
9 |
|
df-sup |
|- sup ( C , A , R ) = U. { x e. A | ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) } |
10 |
7 8 9
|
3eqtr4g |
|- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) ) |