Description: A one-to-one function maps different arguments onto different values. Implication of the alternate definition dff14a . (Contributed by AV, 30-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dff14i | |- ( ( F : A -1-1-> B /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> ( F ` X ) =/= ( F ` Y ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1veqaeq | |- ( ( F : A -1-1-> B /\ ( X e. A /\ Y e. A ) ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) |
|
| 2 | 1 | necon3d | |- ( ( F : A -1-1-> B /\ ( X e. A /\ Y e. A ) ) -> ( X =/= Y -> ( F ` X ) =/= ( F ` Y ) ) ) |
| 3 | 2 | exp32 | |- ( F : A -1-1-> B -> ( X e. A -> ( Y e. A -> ( X =/= Y -> ( F ` X ) =/= ( F ` Y ) ) ) ) ) |
| 4 | 3 | 3imp2 | |- ( ( F : A -1-1-> B /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> ( F ` X ) =/= ( F ` Y ) ) |