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\to \left(H:A⟶B\leftrightarrow G:A⟶B\right)$$
2		fveq1	$$⊢H=G\to H\left(x\right)=G\left(x\right)$$
3		fveq1	$$⊢H=G\to H\left(y\right)=G\left(y\right)$$
4	2 3	breq12d	$$⊢H=G\to \left(H\left(x\right)SH\left(y\right)\leftrightarrow G\left(x\right)SG\left(y\right)\right)$$
5	4	imbi2d	$$⊢H=G\to \left(\left(xRy\to H\left(x\right)SH\left(y\right)\right)\leftrightarrow \left(xRy\to G\left(x\right)SG\left(y\right)\right)\right)$$
6	5	2ralbidv	$$⊢H=G\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 G\left(x\right)SG\left(y\right)\right)\right)$$
7	1 6	anbi12d	$$⊢H=G\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(G:A⟶B\wedge \forall x\in A\forall y\in A\left(xRy\to G\left(x\right)SG\left(y\right)\right)\right)\right)$$
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 |-