Step | Hyp | Ref
| Expression |
1 | | dff13 7120 |
. 2
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((𝐹‘𝑤) = (𝐹‘𝑣) → 𝑤 = 𝑣))) |
2 | | dff13f.2 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐹 |
3 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝑤 |
4 | 2, 3 | nffv 6776 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝐹‘𝑤) |
5 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝑣 |
6 | 2, 5 | nffv 6776 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝐹‘𝑣) |
7 | 4, 6 | nfeq 2920 |
. . . . . . 7
⊢
Ⅎ𝑦(𝐹‘𝑤) = (𝐹‘𝑣) |
8 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑦 𝑤 = 𝑣 |
9 | 7, 8 | nfim 1899 |
. . . . . 6
⊢
Ⅎ𝑦((𝐹‘𝑤) = (𝐹‘𝑣) → 𝑤 = 𝑣) |
10 | | nfv 1917 |
. . . . . 6
⊢
Ⅎ𝑣((𝐹‘𝑤) = (𝐹‘𝑦) → 𝑤 = 𝑦) |
11 | | fveq2 6766 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦)) |
12 | 11 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → ((𝐹‘𝑤) = (𝐹‘𝑣) ↔ (𝐹‘𝑤) = (𝐹‘𝑦))) |
13 | | equequ2 2029 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → (𝑤 = 𝑣 ↔ 𝑤 = 𝑦)) |
14 | 12, 13 | imbi12d 345 |
. . . . . 6
⊢ (𝑣 = 𝑦 → (((𝐹‘𝑤) = (𝐹‘𝑣) → 𝑤 = 𝑣) ↔ ((𝐹‘𝑤) = (𝐹‘𝑦) → 𝑤 = 𝑦))) |
15 | 9, 10, 14 | cbvralw 3371 |
. . . . 5
⊢
(∀𝑣 ∈
𝐴 ((𝐹‘𝑤) = (𝐹‘𝑣) → 𝑤 = 𝑣) ↔ ∀𝑦 ∈ 𝐴 ((𝐹‘𝑤) = (𝐹‘𝑦) → 𝑤 = 𝑦)) |
16 | 15 | ralbii 3091 |
. . . 4
⊢
(∀𝑤 ∈
𝐴 ∀𝑣 ∈ 𝐴 ((𝐹‘𝑤) = (𝐹‘𝑣) → 𝑤 = 𝑣) ↔ ∀𝑤 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑤) = (𝐹‘𝑦) → 𝑤 = 𝑦)) |
17 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
18 | | dff13f.1 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐹 |
19 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑤 |
20 | 18, 19 | nffv 6776 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐹‘𝑤) |
21 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑦 |
22 | 18, 21 | nffv 6776 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐹‘𝑦) |
23 | 20, 22 | nfeq 2920 |
. . . . . . 7
⊢
Ⅎ𝑥(𝐹‘𝑤) = (𝐹‘𝑦) |
24 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑤 = 𝑦 |
25 | 23, 24 | nfim 1899 |
. . . . . 6
⊢
Ⅎ𝑥((𝐹‘𝑤) = (𝐹‘𝑦) → 𝑤 = 𝑦) |
26 | 17, 25 | nfralw 3150 |
. . . . 5
⊢
Ⅎ𝑥∀𝑦 ∈ 𝐴 ((𝐹‘𝑤) = (𝐹‘𝑦) → 𝑤 = 𝑦) |
27 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑤∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) |
28 | | fveqeq2 6775 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ((𝐹‘𝑤) = (𝐹‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
29 | | equequ1 2028 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (𝑤 = 𝑦 ↔ 𝑥 = 𝑦)) |
30 | 28, 29 | imbi12d 345 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (((𝐹‘𝑤) = (𝐹‘𝑦) → 𝑤 = 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
31 | 30 | ralbidv 3121 |
. . . . 5
⊢ (𝑤 = 𝑥 → (∀𝑦 ∈ 𝐴 ((𝐹‘𝑤) = (𝐹‘𝑦) → 𝑤 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
32 | 26, 27, 31 | cbvralw 3371 |
. . . 4
⊢
(∀𝑤 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑤) = (𝐹‘𝑦) → 𝑤 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
33 | 16, 32 | bitri 274 |
. . 3
⊢
(∀𝑤 ∈
𝐴 ∀𝑣 ∈ 𝐴 ((𝐹‘𝑤) = (𝐹‘𝑣) → 𝑤 = 𝑣) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
34 | 33 | anbi2i 623 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((𝐹‘𝑤) = (𝐹‘𝑣) → 𝑤 = 𝑣)) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
35 | 1, 34 | bitri 274 |
1
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |