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