Proof of Theorem rmoxfrd
Step | Hyp | Ref
| Expression |
1 | | rmoxfrd.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) |
2 | | rmoxfrd.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) |
3 | | reurex 3361 |
. . . . . . 7
⊢
(∃!𝑦 ∈
𝐶 𝑥 = 𝐴 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) |
5 | | rmoxfrd.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
6 | 1, 4, 5 | rexxfrd 5336 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) |
7 | | df-rex 3072 |
. . . . 5
⊢
(∃𝑥 ∈
𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
8 | | df-rex 3072 |
. . . . 5
⊢
(∃𝑦 ∈
𝐶 𝜒 ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ 𝜒)) |
9 | 6, 7, 8 | 3bitr3g 313 |
. . . 4
⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ 𝜒))) |
10 | 1, 2, 5 | reuxfr1d 3689 |
. . . . 5
⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒)) |
11 | | df-reu 3073 |
. . . . 5
⊢
(∃!𝑥 ∈
𝐵 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
12 | | df-reu 3073 |
. . . . 5
⊢
(∃!𝑦 ∈
𝐶 𝜒 ↔ ∃!𝑦(𝑦 ∈ 𝐶 ∧ 𝜒)) |
13 | 10, 11, 12 | 3bitr3g 313 |
. . . 4
⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓) ↔ ∃!𝑦(𝑦 ∈ 𝐶 ∧ 𝜒))) |
14 | 9, 13 | imbi12d 345 |
. . 3
⊢ (𝜑 → ((∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓) → ∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑦(𝑦 ∈ 𝐶 ∧ 𝜒) → ∃!𝑦(𝑦 ∈ 𝐶 ∧ 𝜒)))) |
15 | | moeu 2585 |
. . 3
⊢
(∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓) → ∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))) |
16 | | moeu 2585 |
. . 3
⊢
(∃*𝑦(𝑦 ∈ 𝐶 ∧ 𝜒) ↔ (∃𝑦(𝑦 ∈ 𝐶 ∧ 𝜒) → ∃!𝑦(𝑦 ∈ 𝐶 ∧ 𝜒))) |
17 | 14, 15, 16 | 3bitr4g 314 |
. 2
⊢ (𝜑 → (∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝜓) ↔ ∃*𝑦(𝑦 ∈ 𝐶 ∧ 𝜒))) |
18 | | df-rmo 3074 |
. 2
⊢
(∃*𝑥 ∈
𝐵 𝜓 ↔ ∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
19 | | df-rmo 3074 |
. 2
⊢
(∃*𝑦 ∈
𝐶 𝜒 ↔ ∃*𝑦(𝑦 ∈ 𝐶 ∧ 𝜒)) |
20 | 17, 18, 19 | 3bitr4g 314 |
1
⊢ (𝜑 → (∃*𝑥 ∈ 𝐵 𝜓 ↔ ∃*𝑦 ∈ 𝐶 𝜒)) |