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 | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1veqaeq | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) | |
| 2 | 1 | necon3d | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑋 ≠ 𝑌 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) |
| 3 | 2 | exp32 | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝑋 ∈ 𝐴 → ( 𝑌 ∈ 𝐴 → ( 𝑋 ≠ 𝑌 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) ) ) |
| 4 | 3 | 3imp2 | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) |