Proof of Theorem reusv3i
Step | Hyp | Ref
| Expression |
1 | | reusv3.1 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) |
2 | | reusv3.2 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) |
3 | 2 | eqeq2d 2176 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝑥 = 𝐶 ↔ 𝑥 = 𝐷)) |
4 | 1, 3 | imbi12d 233 |
. . . . 5
⊢ (𝑦 = 𝑧 → ((𝜑 → 𝑥 = 𝐶) ↔ (𝜓 → 𝑥 = 𝐷))) |
5 | 4 | cbvralv 2690 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 (𝜑 → 𝑥 = 𝐶) ↔ ∀𝑧 ∈ 𝐵 (𝜓 → 𝑥 = 𝐷)) |
6 | 5 | biimpi 119 |
. . 3
⊢
(∀𝑦 ∈
𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑧 ∈ 𝐵 (𝜓 → 𝑥 = 𝐷)) |
7 | | raaanv 3512 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 → 𝑥 = 𝐶) ∧ (𝜓 → 𝑥 = 𝐷)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) ∧ ∀𝑧 ∈ 𝐵 (𝜓 → 𝑥 = 𝐷))) |
8 | | anim12 342 |
. . . . . . 7
⊢ (((𝜑 → 𝑥 = 𝐶) ∧ (𝜓 → 𝑥 = 𝐷)) → ((𝜑 ∧ 𝜓) → (𝑥 = 𝐶 ∧ 𝑥 = 𝐷))) |
9 | | eqtr2 2183 |
. . . . . . 7
⊢ ((𝑥 = 𝐶 ∧ 𝑥 = 𝐷) → 𝐶 = 𝐷) |
10 | 8, 9 | syl6 33 |
. . . . . 6
⊢ (((𝜑 → 𝑥 = 𝐶) ∧ (𝜓 → 𝑥 = 𝐷)) → ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |
11 | 10 | ralimi 2527 |
. . . . 5
⊢
(∀𝑧 ∈
𝐵 ((𝜑 → 𝑥 = 𝐶) ∧ (𝜓 → 𝑥 = 𝐷)) → ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |
12 | 11 | ralimi 2527 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 → 𝑥 = 𝐶) ∧ (𝜓 → 𝑥 = 𝐷)) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |
13 | 7, 12 | sylbir 134 |
. . 3
⊢
((∀𝑦 ∈
𝐵 (𝜑 → 𝑥 = 𝐶) ∧ ∀𝑧 ∈ 𝐵 (𝜓 → 𝑥 = 𝐷)) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |
14 | 6, 13 | mpdan 418 |
. 2
⊢
(∀𝑦 ∈
𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |
15 | 14 | rexlimivw 2577 |
1
⊢
(∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) |