Proof of Theorem caovcan
Step | Hyp | Ref
| Expression |
1 | | oveq1 7142 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥𝐹𝑦) = (𝐴𝐹𝑦)) |
2 | | oveq1 7142 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥𝐹𝐶) = (𝐴𝐹𝐶)) |
3 | 1, 2 | eqeq12d 2814 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦) = (𝑥𝐹𝐶) ↔ (𝐴𝐹𝑦) = (𝐴𝐹𝐶))) |
4 | 3 | imbi1d 345 |
. 2
⊢ (𝑥 = 𝐴 → (((𝑥𝐹𝑦) = (𝑥𝐹𝐶) → 𝑦 = 𝐶) ↔ ((𝐴𝐹𝑦) = (𝐴𝐹𝐶) → 𝑦 = 𝐶))) |
5 | | oveq2 7143 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦) = (𝐴𝐹𝐵)) |
6 | 5 | eqeq1d 2800 |
. . 3
⊢ (𝑦 = 𝐵 → ((𝐴𝐹𝑦) = (𝐴𝐹𝐶) ↔ (𝐴𝐹𝐵) = (𝐴𝐹𝐶))) |
7 | | eqeq1 2802 |
. . 3
⊢ (𝑦 = 𝐵 → (𝑦 = 𝐶 ↔ 𝐵 = 𝐶)) |
8 | 6, 7 | imbi12d 348 |
. 2
⊢ (𝑦 = 𝐵 → (((𝐴𝐹𝑦) = (𝐴𝐹𝐶) → 𝑦 = 𝐶) ↔ ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) → 𝐵 = 𝐶))) |
9 | | caovcan.1 |
. . 3
⊢ 𝐶 ∈ V |
10 | | oveq2 7143 |
. . . . . 6
⊢ (𝑧 = 𝐶 → (𝑥𝐹𝑧) = (𝑥𝐹𝐶)) |
11 | 10 | eqeq2d 2809 |
. . . . 5
⊢ (𝑧 = 𝐶 → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ (𝑥𝐹𝑦) = (𝑥𝐹𝐶))) |
12 | | eqeq2 2810 |
. . . . 5
⊢ (𝑧 = 𝐶 → (𝑦 = 𝑧 ↔ 𝑦 = 𝐶)) |
13 | 11, 12 | imbi12d 348 |
. . . 4
⊢ (𝑧 = 𝐶 → (((𝑥𝐹𝑦) = (𝑥𝐹𝑧) → 𝑦 = 𝑧) ↔ ((𝑥𝐹𝑦) = (𝑥𝐹𝐶) → 𝑦 = 𝐶))) |
14 | 13 | imbi2d 344 |
. . 3
⊢ (𝑧 = 𝐶 → (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) → 𝑦 = 𝑧)) ↔ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝐶) → 𝑦 = 𝐶)))) |
15 | | caovcan.2 |
. . 3
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) → 𝑦 = 𝑧)) |
16 | 9, 14, 15 | vtocl 3507 |
. 2
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝐶) → 𝑦 = 𝐶)) |
17 | 4, 8, 16 | vtocl2ga 3523 |
1
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) → 𝐵 = 𝐶)) |