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 F : A 1-1 B F : A B ¬ x A y A F x = F y x y

Proof

Step Hyp Ref Expression
1 dff13 F : A 1-1 B F : A B x A y A F x = F y x = y
2 iman F x = F y x = y ¬ F x = F y ¬ x = y
3 df-ne x y ¬ x = y
4 3 anbi2i F x = F y x y F x = F y ¬ x = y
5 2 4 xchbinxr F x = F y x = y ¬ F x = F y x y
6 5 2ralbii x A y A F x = F y x = y x A y A ¬ F x = F y x y
7 ralnex2 x A y A ¬ F x = F y x y ¬ x A y A F x = F y x y
8 6 7 bitri x A y A F x = F y x = y ¬ x A y A F x = F y x y
9 8 anbi2i F : A B x A y A F x = F y x = y F : A B ¬ x A y A F x = F y x y
10 1 9 bitri F : A 1-1 B F : A B ¬ x A y A F x = F y x y