Theorem relpeq3

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

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

Proof

Step	Hyp	Ref	Expression
1		breq	$$⊢S=T\to \left(H\left(x\right)SH\left(y\right)\leftrightarrow H\left(x\right)TH\left(y\right)\right)$$
2	1	imbi2d	$$⊢S=T\to \left(\left(xRy\to H\left(x\right)SH\left(y\right)\right)\leftrightarrow \left(xRy\to H\left(x\right)TH\left(y\right)\right)\right)$$
3	2	2ralbidv	$$⊢S=T\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 A\forall y\in A\left(xRy\to H\left(x\right)TH\left(y\right)\right)\right)$$
4	3	anbi2d	$$⊢S=T\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⟶B\wedge \forall x\in A\forall y\in A\left(xRy\to H\left(x\right)TH\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 , T ( A , B ) <-> ( H : A --> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) T ( H ` y ) ) ) ) : No typesetting found for |- ( H RelPres R , T ( A , B ) <-> ( H : A --> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) T ( H ` y ) ) ) ) with typecode |-
7	4 5 6	3bitr4g	Could not format ( S = T -> ( H RelPres R , S ( A , B ) <-> H RelPres R , T ( A , B ) ) ) : No typesetting found for |- ( S = T -> ( H RelPres R , S ( A , B ) <-> H RelPres R , T ( A , B ) ) ) with typecode |-