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\to \left(H:A⟶B\leftrightarrow H:C⟶B\right)$$
2		raleq	$$⊢A=C\to \left(\forall y\in A\left(xRy\to H\left(x\right)SH\left(y\right)\right)\leftrightarrow \forall y\in C\left(xRy\to H\left(x\right)SH\left(y\right)\right)\right)$$
3	2	raleqbi1dv	$$⊢A=C\to \left(\forall x\in A\forall y\in A\left(xRy\to H\left(x\right)SH\left(y\right)\right)\leftrightarrow \forall x\in C\forall y\in C\left(xRy\to H\left(x\right)SH\left(y\right)\right)\right)$$
4	1 3	anbi12d	$$⊢A=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:C⟶B\wedge \forall x\in C\forall y\in C\left(xRy\to H\left(x\right)SH\left(y\right)\right)\right)\right)$$
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 |-