Proof of Theorem raaan
Step | Hyp | Ref
| Expression |
1 | | raaan.1 |
. . . 4
⊢
Ⅎ𝑦𝜑 |
2 | | raaan.2 |
. . . 4
⊢
Ⅎ𝑥𝜓 |
3 | 1, 2 | raaanlem 3326 |
. . 3
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))) |
4 | 3 | pm5.74i 169 |
. 2
⊢
((∃𝑥 𝑥 ∈ 𝐴 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓)) ↔ (∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))) |
5 | | ralm 3325 |
. 2
⊢
((∃𝑥 𝑥 ∈ 𝐴 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
6 | | jcab 535 |
. . 3
⊢
((∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) ↔ ((∃𝑥 𝑥 ∈ 𝐴 → ∀𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑥 𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜓))) |
7 | | ralm 3325 |
. . . 4
⊢
((∃𝑥 𝑥 ∈ 𝐴 → ∀𝑥 ∈ 𝐴 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) |
8 | | eleq1 2100 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
9 | 8 | cbvexv 1795 |
. . . . . 6
⊢
(∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝑦 ∈ 𝐴) |
10 | 9 | imbi1i 227 |
. . . . 5
⊢
((∃𝑥 𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜓) ↔ (∃𝑦 𝑦 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜓)) |
11 | | ralm 3325 |
. . . . 5
⊢
((∃𝑦 𝑦 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜓) ↔ ∀𝑦 ∈ 𝐴 𝜓) |
12 | 10, 11 | bitri 173 |
. . . 4
⊢
((∃𝑥 𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜓) ↔ ∀𝑦 ∈ 𝐴 𝜓) |
13 | 7, 12 | anbi12i 433 |
. . 3
⊢
(((∃𝑥 𝑥 ∈ 𝐴 → ∀𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑥 𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) |
14 | 6, 13 | bitri 173 |
. 2
⊢
((∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) |
15 | 4, 5, 14 | 3bitr3i 199 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) |