Metamath Proof Explorer


Theorem dff15

Description: A one-to-one function in terms of different arguments never having the same function value. (Contributed by BTernaryTau, 24-Oct-2023)

Ref Expression
Assertion dff15 ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ¬ ∃ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 dff13 ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
2 iman ( ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
3 df-ne ( 𝑥𝑦 ↔ ¬ 𝑥 = 𝑦 )
4 3 anbi2i ( ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥𝑦 ) ↔ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
5 2 4 xchbinxr ( ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥𝑦 ) )
6 5 2ralbii ( ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥𝐴𝑦𝐴 ¬ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥𝑦 ) )
7 ralnex2 ( ∀ 𝑥𝐴𝑦𝐴 ¬ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥𝑦 ) ↔ ¬ ∃ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥𝑦 ) )
8 6 7 bitri ( ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ∃ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥𝑦 ) )
9 8 anbi2i ( ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝐹 : 𝐴𝐵 ∧ ¬ ∃ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥𝑦 ) ) )
10 1 9 bitri ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ¬ ∃ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥𝑦 ) ) )