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 𝑥 𝐹
dff13f.2 𝑦 𝐹
Assertion dff13f ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 dff13f.1 𝑥 𝐹
2 dff13f.2 𝑦 𝐹
3 dff13 ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑤𝐴𝑣𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑣 ) → 𝑤 = 𝑣 ) ) )
4 nfcv 𝑦 𝑤
5 2 4 nffv 𝑦 ( 𝐹𝑤 )
6 nfcv 𝑦 𝑣
7 2 6 nffv 𝑦 ( 𝐹𝑣 )
8 5 7 nfeq 𝑦 ( 𝐹𝑤 ) = ( 𝐹𝑣 )
9 nfv 𝑦 𝑤 = 𝑣
10 8 9 nfim 𝑦 ( ( 𝐹𝑤 ) = ( 𝐹𝑣 ) → 𝑤 = 𝑣 )
11 nfv 𝑣 ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) → 𝑤 = 𝑦 )
12 fveq2 ( 𝑣 = 𝑦 → ( 𝐹𝑣 ) = ( 𝐹𝑦 ) )
13 12 eqeq2d ( 𝑣 = 𝑦 → ( ( 𝐹𝑤 ) = ( 𝐹𝑣 ) ↔ ( 𝐹𝑤 ) = ( 𝐹𝑦 ) ) )
14 equequ2 ( 𝑣 = 𝑦 → ( 𝑤 = 𝑣𝑤 = 𝑦 ) )
15 13 14 imbi12d ( 𝑣 = 𝑦 → ( ( ( 𝐹𝑤 ) = ( 𝐹𝑣 ) → 𝑤 = 𝑣 ) ↔ ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) → 𝑤 = 𝑦 ) ) )
16 10 11 15 cbvralw ( ∀ 𝑣𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑣 ) → 𝑤 = 𝑣 ) ↔ ∀ 𝑦𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) → 𝑤 = 𝑦 ) )
17 16 ralbii ( ∀ 𝑤𝐴𝑣𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑣 ) → 𝑤 = 𝑣 ) ↔ ∀ 𝑤𝐴𝑦𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) → 𝑤 = 𝑦 ) )
18 nfcv 𝑥 𝐴
19 nfcv 𝑥 𝑤
20 1 19 nffv 𝑥 ( 𝐹𝑤 )
21 nfcv 𝑥 𝑦
22 1 21 nffv 𝑥 ( 𝐹𝑦 )
23 20 22 nfeq 𝑥 ( 𝐹𝑤 ) = ( 𝐹𝑦 )
24 nfv 𝑥 𝑤 = 𝑦
25 23 24 nfim 𝑥 ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) → 𝑤 = 𝑦 )
26 18 25 nfralw 𝑥𝑦𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) → 𝑤 = 𝑦 )
27 nfv 𝑤𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 )
28 fveqeq2 ( 𝑤 = 𝑥 → ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) ↔ ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ) )
29 equequ1 ( 𝑤 = 𝑥 → ( 𝑤 = 𝑦𝑥 = 𝑦 ) )
30 28 29 imbi12d ( 𝑤 = 𝑥 → ( ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) → 𝑤 = 𝑦 ) ↔ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
31 30 ralbidv ( 𝑤 = 𝑥 → ( ∀ 𝑦𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) → 𝑤 = 𝑦 ) ↔ ∀ 𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
32 26 27 31 cbvralw ( ∀ 𝑤𝐴𝑦𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑦 ) → 𝑤 = 𝑦 ) ↔ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) )
33 17 32 bitri ( ∀ 𝑤𝐴𝑣𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑣 ) → 𝑤 = 𝑣 ) ↔ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) )
34 33 anbi2i ( ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑤𝐴𝑣𝐴 ( ( 𝐹𝑤 ) = ( 𝐹𝑣 ) → 𝑤 = 𝑣 ) ) ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
35 3 34 bitri ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )