Proof of Theorem ceqsrex2v
Step | Hyp | Ref
| Expression |
1 | | anass 469 |
. . . . . 6
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ (𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑))) |
2 | 1 | rexbii 3180 |
. . . . 5
⊢
(∃𝑦 ∈
𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ ∃𝑦 ∈ 𝐷 (𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑))) |
3 | | r19.42v 3279 |
. . . . 5
⊢
(∃𝑦 ∈
𝐷 (𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑)) ↔ (𝑥 = 𝐴 ∧ ∃𝑦 ∈ 𝐷 (𝑦 = 𝐵 ∧ 𝜑))) |
4 | 2, 3 | bitri 274 |
. . . 4
⊢
(∃𝑦 ∈
𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ (𝑥 = 𝐴 ∧ ∃𝑦 ∈ 𝐷 (𝑦 = 𝐵 ∧ 𝜑))) |
5 | 4 | rexbii 3180 |
. . 3
⊢
(∃𝑥 ∈
𝐶 ∃𝑦 ∈ 𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐶 (𝑥 = 𝐴 ∧ ∃𝑦 ∈ 𝐷 (𝑦 = 𝐵 ∧ 𝜑))) |
6 | | ceqsrex2v.1 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
7 | 6 | anbi2d 629 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑦 = 𝐵 ∧ 𝜑) ↔ (𝑦 = 𝐵 ∧ 𝜓))) |
8 | 7 | rexbidv 3228 |
. . . 4
⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 (𝑦 = 𝐵 ∧ 𝜑) ↔ ∃𝑦 ∈ 𝐷 (𝑦 = 𝐵 ∧ 𝜓))) |
9 | 8 | ceqsrexv 3587 |
. . 3
⊢ (𝐴 ∈ 𝐶 → (∃𝑥 ∈ 𝐶 (𝑥 = 𝐴 ∧ ∃𝑦 ∈ 𝐷 (𝑦 = 𝐵 ∧ 𝜑)) ↔ ∃𝑦 ∈ 𝐷 (𝑦 = 𝐵 ∧ 𝜓))) |
10 | 5, 9 | bitrid 282 |
. 2
⊢ (𝐴 ∈ 𝐶 → (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ ∃𝑦 ∈ 𝐷 (𝑦 = 𝐵 ∧ 𝜓))) |
11 | | ceqsrex2v.2 |
. . 3
⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
12 | 11 | ceqsrexv 3587 |
. 2
⊢ (𝐵 ∈ 𝐷 → (∃𝑦 ∈ 𝐷 (𝑦 = 𝐵 ∧ 𝜓) ↔ 𝜒)) |
13 | 10, 12 | sylan9bb 510 |
1
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ 𝜒)) |