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 |- |
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 |- |