Metamath Proof Explorer


Theorem relpeq4

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

Ref Expression
Assertion relpeq4 Could not format assertion : No typesetting found for |- ( A = C -> ( H RelPres R , S ( A , B ) <-> H RelPres R , S ( C , B ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 feq2 A = C H : A B H : C B
2 raleq A = C y A x R y H x S H y y C x R y H x S H y
3 2 raleqbi1dv A = C x A y A x R y H x S H y x C y C x R y H x S H y
4 1 3 anbi12d A = C H : A B x A y A x R y H x S H y H : C B x C y C x R y H x S H y
5 df-relp Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
6 df-relp Could not format ( H RelPres R , S ( C , B ) <-> ( H : C --> B /\ A. x e. C A. y e. C ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) : No typesetting found for |- ( H RelPres R , S ( C , B ) <-> ( H : C --> B /\ A. x e. C A. y e. C ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) with typecode |-
7 4 5 6 3bitr4g Could not format ( A = C -> ( H RelPres R , S ( A , B ) <-> H RelPres R , S ( C , B ) ) ) : No typesetting found for |- ( A = C -> ( H RelPres R , S ( A , B ) <-> H RelPres R , S ( C , B ) ) ) with typecode |-