Metamath Proof Explorer

Theorem relpeq5

Description: Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025)

Ref Expression
Assertion relpeq5 
|- ( B = C -> ( H RelPres R , S ( A , B ) <-> H RelPres R , S ( A , C ) ) )

Proof

Step Hyp Ref Expression
1 feq3 
 |-  ( B = C -> ( H : A --> B <-> H : A --> C ) )
2 1 anbi1d 
 |-  ( B = C -> ( ( H : A --> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) <-> ( H : A --> C /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) )
3 df-relp 
 |-  ( H RelPres R , S ( A , B ) <-> ( H : A --> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) )
4 df-relp 
 |-  ( H RelPres R , S ( A , C ) <-> ( H : A --> C /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) )
5 2 3 4 3bitr4g 
 |-  ( B = C -> ( H RelPres R , S ( A , B ) <-> H RelPres R , S ( A , C ) ) )