Metamath Proof Explorer


Theorem relpeq1

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

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

Proof

Step Hyp Ref Expression
1 feq1 H = G H : A B G : A B
2 fveq1 H = G H x = G x
3 fveq1 H = G H y = G y
4 2 3 breq12d H = G H x S H y G x S G y
5 4 imbi2d H = G x R y H x S H y x R y G x S G y
6 5 2ralbidv H = G x A y A x R y H x S H y x A y A x R y G x S G y
7 1 6 anbi12d H = G H : A B x A y A x R y H x S H y G : A B x A y A x R y G x S G y
8 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 |-
9 df-relp Could not format ( G RelPres R , S ( A , B ) <-> ( G : A --> B /\ A. x e. A A. y e. A ( x R y -> ( G ` x ) S ( G ` y ) ) ) ) : No typesetting found for |- ( G RelPres R , S ( A , B ) <-> ( G : A --> B /\ A. x e. A A. y e. A ( x R y -> ( G ` x ) S ( G ` y ) ) ) ) with typecode |-
10 7 8 9 3bitr4g Could not format ( H = G -> ( H RelPres R , S ( A , B ) <-> G RelPres R , S ( A , B ) ) ) : No typesetting found for |- ( H = G -> ( H RelPres R , S ( A , B ) <-> G RelPres R , S ( A , B ) ) ) with typecode |-