Theorem relpeq5

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

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

Proof

Step	Hyp	Ref	Expression
1		feq3	$$⊢B=C\to \left(H:A⟶B\leftrightarrow H:A⟶C\right)$$
2	1	anbi1d	$$⊢B=C\to \left(\left(H:A⟶B\wedge \forall x\in A\forall y\in A\left(xRy\to H\left(x\right)SH\left(y\right)\right)\right)\leftrightarrow \left(H:A⟶C\wedge \forall x\in A\forall y\in A\left(xRy\to H\left(x\right)SH\left(y\right)\right)\right)\right)$$
3		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 |-
4		df-relp	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
5	2 3 4	3bitr4g	Could not format ( B = C -> ( H RelPres R , S ( A , B ) <-> H RelPres R , S ( A , C ) ) ) : No typesetting found for |- ( B = C -> ( H RelPres R , S ( A , B ) <-> H RelPres R , S ( A , C ) ) ) with typecode |-