Metamath Proof Explorer


Theorem dff13

Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of Monk1 p. 43. (Contributed by NM, 29-Oct-1996)

Ref Expression
Assertion dff13 F : A 1-1 B F : A B x A y A F x = F y x = y

Proof

Step Hyp Ref Expression
1 dff12 F : A 1-1 B F : A B z * x x F z
2 ffn F : A B F Fn A
3 vex x V
4 vex z V
5 3 4 breldm x F z x dom F
6 fndm F Fn A dom F = A
7 6 eleq2d F Fn A x dom F x A
8 5 7 syl5ib F Fn A x F z x A
9 vex y V
10 9 4 breldm y F z y dom F
11 6 eleq2d F Fn A y dom F y A
12 10 11 syl5ib F Fn A y F z y A
13 8 12 anim12d F Fn A x F z y F z x A y A
14 13 pm4.71rd F Fn A x F z y F z x A y A x F z y F z
15 eqcom z = F x F x = z
16 fnbrfvb F Fn A x A F x = z x F z
17 15 16 bitrid F Fn A x A z = F x x F z
18 eqcom z = F y F y = z
19 fnbrfvb F Fn A y A F y = z y F z
20 18 19 bitrid F Fn A y A z = F y y F z
21 17 20 bi2anan9 F Fn A x A F Fn A y A z = F x z = F y x F z y F z
22 21 anandis F Fn A x A y A z = F x z = F y x F z y F z
23 22 pm5.32da F Fn A x A y A z = F x z = F y x A y A x F z y F z
24 14 23 bitr4d F Fn A x F z y F z x A y A z = F x z = F y
25 24 imbi1d F Fn A x F z y F z x = y x A y A z = F x z = F y x = y
26 impexp x A y A z = F x z = F y x = y x A y A z = F x z = F y x = y
27 25 26 bitrdi F Fn A x F z y F z x = y x A y A z = F x z = F y x = y
28 27 albidv F Fn A z x F z y F z x = y z x A y A z = F x z = F y x = y
29 19.21v z x A y A z = F x z = F y x = y x A y A z z = F x z = F y x = y
30 19.23v z z = F x z = F y x = y z z = F x z = F y x = y
31 fvex F x V
32 31 eqvinc F x = F y z z = F x z = F y
33 32 imbi1i F x = F y x = y z z = F x z = F y x = y
34 30 33 bitr4i z z = F x z = F y x = y F x = F y x = y
35 34 imbi2i x A y A z z = F x z = F y x = y x A y A F x = F y x = y
36 29 35 bitri z x A y A z = F x z = F y x = y x A y A F x = F y x = y
37 28 36 bitrdi F Fn A z x F z y F z x = y x A y A F x = F y x = y
38 37 2albidv F Fn A x y z x F z y F z x = y x y x A y A F x = F y x = y
39 breq1 x = y x F z y F z
40 39 mo4 * x x F z x y x F z y F z x = y
41 40 albii z * x x F z z x y x F z y F z x = y
42 alrot3 z x y x F z y F z x = y x y z x F z y F z x = y
43 41 42 bitri z * x x F z x y z x F z y F z x = y
44 r2al x A y A F x = F y x = y x y x A y A F x = F y x = y
45 38 43 44 3bitr4g F Fn A z * x x F z x A y A F x = F y x = y
46 2 45 syl F : A B z * x x F z x A y A F x = F y x = y
47 46 pm5.32i F : A B z * x x F z F : A B x A y A F x = F y x = y
48 1 47 bitri F : A 1-1 B F : A B x A y A F x = F y x = y