Proof of Theorem reuxfrd
| Step | Hyp | Ref
| Expression |
| 1 | | reuxfrd.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 𝑥 = 𝐴) |
| 2 | | rmoan 3745 |
. . . . . . 7
⊢
(∃*𝑦 ∈
𝐶 𝑥 = 𝐴 → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴)) |
| 3 | 1, 2 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴)) |
| 4 | | ancom 460 |
. . . . . . 7
⊢ ((𝜓 ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ 𝜓)) |
| 5 | 4 | rmobii 3388 |
. . . . . 6
⊢
(∃*𝑦 ∈
𝐶 (𝜓 ∧ 𝑥 = 𝐴) ↔ ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) |
| 6 | 3, 5 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) |
| 7 | 6 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) |
| 8 | | 2reuswap 3752 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓))) |
| 9 | 7, 8 | syl 17 |
. . 3
⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓))) |
| 10 | | 2reuswap2 3753 |
. . . 4
⊢
(∀𝑦 ∈
𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))) |
| 11 | | moeq 3713 |
. . . . . . 7
⊢
∃*𝑥 𝑥 = 𝐴 |
| 12 | 11 | moani 2553 |
. . . . . 6
⊢
∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) |
| 13 | | ancom 460 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓))) |
| 14 | | an12 645 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
| 15 | 13, 14 | bitri 275 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
| 16 | 15 | mobii 2548 |
. . . . . 6
⊢
(∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
| 17 | 12, 16 | mpbi 230 |
. . . . 5
⊢
∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) |
| 18 | 17 | a1i 11 |
. . . 4
⊢ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) |
| 19 | 10, 18 | mprg 3067 |
. . 3
⊢
(∃!𝑦 ∈
𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) |
| 20 | 9, 19 | impbid1 225 |
. 2
⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓))) |
| 21 | | reuxfrd.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) |
| 22 | | biidd 262 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜓)) |
| 23 | 22 | ceqsrexv 3655 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓)) |
| 24 | 21, 23 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓)) |
| 25 | 24 | reubidva 3396 |
. 2
⊢ (𝜑 → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓)) |
| 26 | 20, 25 | bitrd 279 |
1
⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓)) |