Proof of Theorem reuxfr2d
Step | Hyp | Ref
| Expression |
1 | | reuxfr2d.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐵 𝑥 = 𝐴) |
2 | | rmoan 3406 |
. . . . . . 7
⊢
(∃*𝑦 ∈
𝐵 𝑥 = 𝐴 → ∃*𝑦 ∈ 𝐵 (𝜓 ∧ 𝑥 = 𝐴)) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐵 (𝜓 ∧ 𝑥 = 𝐴)) |
4 | | ancom 466 |
. . . . . . 7
⊢ ((𝜓 ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ 𝜓)) |
5 | 4 | rmobii 3133 |
. . . . . 6
⊢
(∃*𝑦 ∈
𝐵 (𝜓 ∧ 𝑥 = 𝐴) ↔ ∃*𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) |
6 | 3, 5 | sylib 208 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) |
7 | 6 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) |
8 | | 2reuswap 3410 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓))) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓))) |
10 | | df-rmo 2920 |
. . . . . 6
⊢
(∃*𝑥 ∈
𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
11 | 10 | ralbii 2980 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 ∃*𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∀𝑦 ∈ 𝐵 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
12 | | 2reuswap 3410 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 ∃*𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓))) |
13 | 11, 12 | sylbir 225 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓))) |
14 | | moeq 3382 |
. . . . . . 7
⊢
∃*𝑥 𝑥 = 𝐴 |
15 | 14 | moani 2525 |
. . . . . 6
⊢
∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) |
16 | | ancom 466 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓))) |
17 | | an12 838 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
18 | 16, 17 | bitri 264 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
19 | 18 | mobii 2493 |
. . . . . 6
⊢
(∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
20 | 15, 19 | mpbi 220 |
. . . . 5
⊢
∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) |
21 | 20 | a1i 11 |
. . . 4
⊢ (𝑦 ∈ 𝐵 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
22 | 13, 21 | mprg 2926 |
. . 3
⊢
(∃!𝑦 ∈
𝐵 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) |
23 | 9, 22 | impbid1 215 |
. 2
⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓))) |
24 | | reuxfr2d.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐴 ∈ 𝐵) |
25 | | biidd 252 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜓)) |
26 | 25 | ceqsrexv 3336 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓)) |
27 | 24, 26 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓)) |
28 | 27 | reubidva 3125 |
. 2
⊢ (𝜑 → (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐵 𝜓)) |
29 | 23, 28 | bitrd 268 |
1
⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐵 𝜓)) |