Metamath Proof Explorer

Theorem dff13f

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

Ref Expression
Hypotheses dff13f.1 
|- F/_ x F
dff13f.2 
|- F/_ y F
Assertion dff13f 
|- ( 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 dff13f.1 
 |-  F/_ x F
2 dff13f.2 
 |-  F/_ y F
3 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. w e. A A. v e. A ( ( F ` w ) = ( F ` v ) -> w = v ) ) )
4 nfcv 
 |-  F/_ y w
5 2 4 nffv 
 |-  F/_ y ( F ` w )
6 nfcv 
 |-  F/_ y v
7 2 6 nffv 
 |-  F/_ y ( F ` v )
8 5 7 nfeq 
 |-  F/ y ( F ` w ) = ( F ` v )
9 nfv 
 |-  F/ y w = v
10 8 9 nfim 
 |-  F/ y ( ( F ` w ) = ( F ` v ) -> w = v )
11 nfv 
 |-  F/ v ( ( F ` w ) = ( F ` y ) -> w = y )
12 fveq2 
 |-  ( v = y -> ( F ` v ) = ( F ` y ) )
13 12 eqeq2d 
 |-  ( v = y -> ( ( F ` w ) = ( F ` v ) <-> ( F ` w ) = ( F ` y ) ) )
14 equequ2 
 |-  ( v = y -> ( w = v <-> w = y ) )
15 13 14 imbi12d 
 |-  ( v = y -> ( ( ( F ` w ) = ( F ` v ) -> w = v ) <-> ( ( F ` w ) = ( F ` y ) -> w = y ) ) )
16 10 11 15 cbvralw 
 |-  ( A. v e. A ( ( F ` w ) = ( F ` v ) -> w = v ) <-> A. y e. A ( ( F ` w ) = ( F ` y ) -> w = y ) )
17 16 ralbii 
 |-  ( A. w e. A A. v e. A ( ( F ` w ) = ( F ` v ) -> w = v ) <-> A. w e. A A. y e. A ( ( F ` w ) = ( F ` y ) -> w = y ) )
18 nfcv 
 |-  F/_ x A
19 nfcv 
 |-  F/_ x w
20 1 19 nffv 
 |-  F/_ x ( F ` w )
21 nfcv 
 |-  F/_ x y
22 1 21 nffv 
 |-  F/_ x ( F ` y )
23 20 22 nfeq 
 |-  F/ x ( F ` w ) = ( F ` y )
24 nfv 
 |-  F/ x w = y
25 23 24 nfim 
 |-  F/ x ( ( F ` w ) = ( F ` y ) -> w = y )
26 18 25 nfralw 
 |-  F/ x A. y e. A ( ( F ` w ) = ( F ` y ) -> w = y )
27 nfv 
 |-  F/ w A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y )
28 fveqeq2 
 |-  ( w = x -> ( ( F ` w ) = ( F ` y ) <-> ( F ` x ) = ( F ` y ) ) )
29 equequ1 
 |-  ( w = x -> ( w = y <-> x = y ) )
30 28 29 imbi12d 
 |-  ( w = x -> ( ( ( F ` w ) = ( F ` y ) -> w = y ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
31 30 ralbidv 
 |-  ( w = x -> ( A. y e. A ( ( F ` w ) = ( F ` y ) -> w = y ) <-> A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
32 26 27 31 cbvralw 
 |-  ( A. w e. A A. y e. A ( ( F ` w ) = ( F ` y ) -> w = y ) <-> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) )
33 17 32 bitri 
 |-  ( A. w e. A A. v e. A ( ( F ` w ) = ( F ` v ) -> w = v ) <-> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) )
34 33 anbi2i 
 |-  ( ( F : A --> B /\ A. w e. A A. v e. A ( ( F ` w ) = ( F ` v ) -> w = v ) ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
35 3 34 bitri 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )