Proof of Theorem reusv3i
Step | Hyp | Ref
| Expression |
1 | | reusv3.1 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) |
2 | | reusv3.2 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) |
3 | 2 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝑥 = 𝐶 ↔ 𝑥 = 𝐷)) |
4 | 1, 3 | imbi12d 345 |
. . . . 5
⊢ (𝑦 = 𝑧 → ((𝜑 → 𝑥 = 𝐶) ↔ (𝜓 → 𝑥 = 𝐷))) |
5 | 4 | cbvralvw 3383 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 (𝜑 → 𝑥 = 𝐶) ↔ ∀𝑧 ∈ 𝐵 (𝜓 → 𝑥 = 𝐷)) |
6 | 5 | biimpi 215 |
. . 3
⊢
(∀𝑦 ∈
𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑧 ∈ 𝐵 (𝜓 → 𝑥 = 𝐷)) |
7 | | raaanv 4452 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 → 𝑥 = 𝐶) ∧ (𝜓 → 𝑥 = 𝐷)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) ∧ ∀𝑧 ∈ 𝐵 (𝜓 → 𝑥 = 𝐷))) |
8 | | anim12 806 |
. . . . . 6
⊢ (((𝜑 → 𝑥 = 𝐶) ∧ (𝜓 → 𝑥 = 𝐷)) → ((𝜑 ∧ 𝜓) → (𝑥 = 𝐶 ∧ 𝑥 = 𝐷))) |
9 | | eqtr2 2762 |
. . . . . 6
⊢ ((𝑥 = 𝐶 ∧ 𝑥 = 𝐷) → 𝐶 = 𝐷) |
10 | 8, 9 | syl6 35 |
. . . . 5
⊢ (((𝜑 → 𝑥 = 𝐶) ∧ (𝜓 → 𝑥 = 𝐷)) → ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |
11 | 10 | 2ralimi 3088 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 → 𝑥 = 𝐶) ∧ (𝜓 → 𝑥 = 𝐷)) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |
12 | 7, 11 | sylbir 234 |
. . 3
⊢
((∀𝑦 ∈
𝐵 (𝜑 → 𝑥 = 𝐶) ∧ ∀𝑧 ∈ 𝐵 (𝜓 → 𝑥 = 𝐷)) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |
13 | 6, 12 | mpdan 684 |
. 2
⊢
(∀𝑦 ∈
𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |
14 | 13 | rexlimivw 3211 |
1
⊢
(∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |