Proof of Theorem raaan
Step | Hyp | Ref
| Expression |
1 | | raaan.1 |
. . . 4
⊢
Ⅎyφ |
2 | | raaan.2 |
. . . 4
⊢
Ⅎxψ |
3 | 1, 2 | raaanlem 3320 |
. . 3
⊢ (∃x x ∈ A → (∀x ∈ A ∀y ∈ A (φ ∧ ψ) ↔ (∀x ∈ A φ ∧ ∀y ∈ A ψ))) |
4 | 3 | pm5.74i 169 |
. 2
⊢ ((∃x x ∈ A → ∀x ∈ A ∀y ∈ A (φ ∧ ψ)) ↔ (∃x x ∈ A → (∀x ∈ A φ ∧ ∀y ∈ A ψ))) |
5 | | ralm 3319 |
. 2
⊢ ((∃x x ∈ A → ∀x ∈ A ∀y ∈ A (φ ∧ ψ)) ↔ ∀x ∈ A ∀y ∈ A (φ ∧ ψ)) |
6 | | jcab 535 |
. . 3
⊢ ((∃x x ∈ A → (∀x ∈ A φ ∧ ∀y ∈ A ψ)) ↔ ((∃x x ∈ A → ∀x ∈ A φ) ∧ (∃x x ∈ A → ∀y ∈ A ψ))) |
7 | | ralm 3319 |
. . . 4
⊢ ((∃x x ∈ A → ∀x ∈ A φ) ↔ ∀x ∈ A φ) |
8 | | eleq1 2097 |
. . . . . . 7
⊢ (x = y →
(x ∈
A ↔ y ∈ A)) |
9 | 8 | cbvexv 1792 |
. . . . . 6
⊢ (∃x x ∈ A ↔ ∃y y ∈ A) |
10 | 9 | imbi1i 227 |
. . . . 5
⊢ ((∃x x ∈ A → ∀y ∈ A ψ) ↔ (∃y y ∈ A → ∀y ∈ A ψ)) |
11 | | ralm 3319 |
. . . . 5
⊢ ((∃y y ∈ A → ∀y ∈ A ψ) ↔ ∀y ∈ A ψ) |
12 | 10, 11 | bitri 173 |
. . . 4
⊢ ((∃x x ∈ A → ∀y ∈ A ψ) ↔ ∀y ∈ A ψ) |
13 | 7, 12 | anbi12i 433 |
. . 3
⊢ (((∃x x ∈ A → ∀x ∈ A φ) ∧ (∃x x ∈ A → ∀y ∈ A ψ)) ↔ (∀x ∈ A φ ∧ ∀y ∈ A ψ)) |
14 | 6, 13 | bitri 173 |
. 2
⊢ ((∃x x ∈ A → (∀x ∈ A φ ∧ ∀y ∈ A ψ)) ↔ (∀x ∈ A φ ∧ ∀y ∈ A ψ)) |
15 | 4, 5, 14 | 3bitr3i 199 |
1
⊢ (∀x ∈ A ∀y ∈ A (φ ∧ ψ) ↔ (∀x ∈ A φ ∧ ∀y ∈ A ψ)) |