Metamath Proof Explorer

Theorem relpf

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

Ref Expression
Assertion relpf 
|- ( H RelPres R , S ( A , B ) -> H : A --> B )

Proof

Step Hyp Ref Expression
1 df-relp 
 |-  ( 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 ) ) ) )
2 1 simplbi 
 |-  ( H RelPres R , S ( A , B ) -> H : A --> B )