Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦) |
2 | | cbvraldva2.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) |
3 | 1, 2 | eleq12d 2831 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
4 | | cbvraldva2.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) |
5 | 3, 4 | anbi12d 631 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
6 | 5 | ancoms 459 |
. . . . . 6
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
7 | 6 | pm5.32da 579 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝜒)))) |
8 | 7 | cbvexvw 2039 |
. . . 4
⊢
(∃𝑥(𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
9 | | 19.42v 1956 |
. . . 4
⊢
(∃𝑥(𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝜑 ∧ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))) |
10 | | 19.42v 1956 |
. . . 4
⊢
(∃𝑦(𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝜒)) ↔ (𝜑 ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒))) |
11 | 8, 9, 10 | 3bitr3i 300 |
. . 3
⊢ ((𝜑 ∧ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝜑 ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒))) |
12 | | pm5.32 574 |
. . 3
⊢ ((𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒))) ↔ ((𝜑 ∧ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝜑 ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒)))) |
13 | 11, 12 | mpbir 230 |
. 2
⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒))) |
14 | | df-rex 3071 |
. 2
⊢
(∃𝑥 ∈
𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) |
15 | | df-rex 3071 |
. 2
⊢
(∃𝑦 ∈
𝐵 𝜒 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜒)) |
16 | 13, 14, 15 | 3bitr4g 313 |
1
⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |