Metamath Proof Explorer


Theorem supeq1

Description: Equality theorem for supremum. (Contributed by NM, 22-May-1999)

Ref Expression
Assertion supeq1
|- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )

Proof

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