Metamath Proof Explorer


Theorem relpf

Description: A relation-preserving function is a function. (Contributed by Eric Schmidt, 11-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 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 |-
2 1 simplbi Could not format ( H RelPres R , S ( A , B ) -> H : A --> B ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> H : A --> B ) with typecode |-