# 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 /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )`

### Proof

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