Step | Hyp | Ref
| Expression |
1 | | df-rmo 2463 |
. 2
⊢
(∃*𝑥 ∈
𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
2 | | simprl 529 |
. . . 4
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → 𝐵 ∈ 𝐴) |
3 | | eleq1 2240 |
. . . 4
⊢ (𝐵 = 𝐶 → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) |
4 | 2, 3 | syl5ibcom 155 |
. . 3
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 → 𝐶 ∈ 𝐴)) |
5 | | simpl 109 |
. . . 4
⊢ ((𝐶 ∈ 𝐴 ∧ 𝜒) → 𝐶 ∈ 𝐴) |
6 | 5 | a1i 9 |
. . 3
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → ((𝐶 ∈ 𝐴 ∧ 𝜒) → 𝐶 ∈ 𝐴)) |
7 | | simplrl 535 |
. . . . 5
⊢
(((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴) |
8 | | simpr 110 |
. . . . 5
⊢
(((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐴) |
9 | | simpll 527 |
. . . . 5
⊢
(((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) ∧ 𝐶 ∈ 𝐴) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
10 | | simplrr 536 |
. . . . 5
⊢
(((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) ∧ 𝐶 ∈ 𝐴) → 𝜓) |
11 | | eleq1 2240 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
12 | | rmoi.b |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) |
13 | 11, 12 | anbi12d 473 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝐵 ∈ 𝐴 ∧ 𝜓))) |
14 | | eleq1 2240 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) |
15 | | rmoi.c |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒)) |
16 | 14, 15 | anbi12d 473 |
. . . . . 6
⊢ (𝑥 = 𝐶 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |
17 | 13, 16 | mob 2919 |
. . . . 5
⊢ (((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |
18 | 7, 8, 9, 7, 10, 17 | syl212anc 1248 |
. . . 4
⊢
(((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) ∧ 𝐶 ∈ 𝐴) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |
19 | 18 | ex 115 |
. . 3
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐶 ∈ 𝐴 → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒)))) |
20 | 4, 6, 19 | pm5.21ndd 705 |
. 2
⊢
((∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |
21 | 1, 20 | sylanb 284 |
1
⊢
((∃*𝑥 ∈
𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |