Step | Hyp | Ref
| Expression |
1 | | impexp 450 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) ↔ (𝜑 → (𝜓 → 𝑥 = 𝑦))) |
2 | 1 | ralbii 3092 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → (𝜓 → 𝑥 = 𝑦))) |
3 | | rmoanim.1 |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
4 | 3 | r19.21 3140 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 (𝜑 → (𝜓 → 𝑥 = 𝑦)) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
5 | 2, 4 | bitri 274 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
6 | 5 | exbii 1853 |
. 2
⊢
(∃𝑦∀𝑥 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) ↔ ∃𝑦(𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
7 | | df-rmo 3073 |
. . 3
⊢
(∃*𝑥 ∈
𝐴 (𝜑 ∧ 𝜓) ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) |
8 | | df-mo 2541 |
. . 3
⊢
(∃*𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) → 𝑥 = 𝑦)) |
9 | | impexp 450 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
10 | 9 | albii 1825 |
. . . . 5
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
11 | | df-ral 3070 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
12 | 10, 11 | bitr4i 277 |
. . . 4
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) |
13 | 12 | exbii 1853 |
. . 3
⊢
(∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ ∃𝑦∀𝑥 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) |
14 | 7, 8, 13 | 3bitri 296 |
. 2
⊢
(∃*𝑥 ∈
𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑦∀𝑥 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) |
15 | | df-rmo 3073 |
. . . . 5
⊢
(∃*𝑥 ∈
𝐴 𝜓 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) |
16 | | df-mo 2541 |
. . . . 5
⊢
(∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 = 𝑦)) |
17 | | impexp 450 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝑥 = 𝑦))) |
18 | 17 | albii 1825 |
. . . . . . 7
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜓 → 𝑥 = 𝑦))) |
19 | | df-ral 3070 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜓 → 𝑥 = 𝑦))) |
20 | 18, 19 | bitr4i 277 |
. . . . . 6
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) |
21 | 20 | exbii 1853 |
. . . . 5
⊢
(∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 = 𝑦) ↔ ∃𝑦∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) |
22 | 15, 16, 21 | 3bitri 296 |
. . . 4
⊢
(∃*𝑥 ∈
𝐴 𝜓 ↔ ∃𝑦∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) |
23 | 22 | imbi2i 335 |
. . 3
⊢ ((𝜑 → ∃*𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∃𝑦∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
24 | | 19.37v 1998 |
. . 3
⊢
(∃𝑦(𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) ↔ (𝜑 → ∃𝑦∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
25 | 23, 24 | bitr4i 277 |
. 2
⊢ ((𝜑 → ∃*𝑥 ∈ 𝐴 𝜓) ↔ ∃𝑦(𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
26 | 6, 14, 25 | 3bitr4i 302 |
1
⊢
(∃*𝑥 ∈
𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)) |