Proof of Theorem rmob
Step | Hyp | Ref
| Expression |
1 | | df-rmo 2904 |
. 2
⊢
(∃*𝑥 ∈
𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
2 | | simprl 790 |
. . . 4
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → 𝐵 ∈ 𝐴) |
3 | | eleq1 2676 |
. . . 4
⊢ (𝐵 = 𝐶 → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) |
4 | 2, 3 | syl5ibcom 234 |
. . 3
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 → 𝐶 ∈ 𝐴)) |
5 | | simpl 472 |
. . . 4
⊢ ((𝐶 ∈ 𝐴 ∧ 𝜒) → 𝐶 ∈ 𝐴) |
6 | 5 | a1i 11 |
. . 3
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → ((𝐶 ∈ 𝐴 ∧ 𝜒) → 𝐶 ∈ 𝐴)) |
7 | 2 | anim1i 590 |
. . . . 5
⊢
(((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) ∧ 𝐶 ∈ 𝐴) → (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) |
8 | | simpll 786 |
. . . . 5
⊢
(((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) ∧ 𝐶 ∈ 𝐴) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
9 | | simplr 788 |
. . . . 5
⊢
(((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) ∧ 𝐶 ∈ 𝐴) → (𝐵 ∈ 𝐴 ∧ 𝜓)) |
10 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
11 | | rmoi.b |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) |
12 | 10, 11 | anbi12d 743 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝐵 ∈ 𝐴 ∧ 𝜓))) |
13 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) |
14 | | rmoi.c |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒)) |
15 | 13, 14 | anbi12d 743 |
. . . . . 6
⊢ (𝑥 = 𝐶 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |
16 | 12, 15 | mob 3355 |
. . . . 5
⊢ (((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |
17 | 7, 8, 9, 16 | syl3anc 1318 |
. . . 4
⊢
(((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) ∧ 𝐶 ∈ 𝐴) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |
18 | 17 | ex 449 |
. . 3
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐶 ∈ 𝐴 → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒)))) |
19 | 4, 6, 18 | pm5.21ndd 368 |
. 2
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |
20 | 1, 19 | sylanb 488 |
1
⊢
((∃*𝑥 ∈
𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |