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