Proof of Theorem 2reu5lem2
Step | Hyp | Ref
| Expression |
1 | | df-rmo 3062 |
. . 3
⊢
(∃*𝑦 ∈
𝐵 𝜑 ↔ ∃*𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) |
2 | 1 | ralbii 3081 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) |
3 | | df-ral 3059 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))) |
4 | | moanimv 2623 |
. . . . . 6
⊢
(∃*𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∃*𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))) |
5 | 4 | bicomi 227 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 → ∃*𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ ∃*𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑))) |
6 | | 3anass 1096 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑))) |
7 | 6 | bicomi 227 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑)) |
8 | 7 | mobii 2549 |
. . . . 5
⊢
(∃*𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ ∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑)) |
9 | 5, 8 | bitri 278 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 → ∃*𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ ∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑)) |
10 | 9 | albii 1826 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑)) |
11 | 3, 10 | bitri 278 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑)) |
12 | 2, 11 | bitri 278 |
1
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑)) |