Proof of Theorem reuss2
Step | Hyp | Ref
| Expression |
1 | | df-rex 3070 |
. . 3
⊢
(∃𝑥 ∈
𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
2 | | df-reu 3072 |
. . 3
⊢
(∃!𝑥 ∈
𝐵 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | 1, 2 | anbi12i 627 |
. 2
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))) |
4 | | df-ral 3069 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓))) |
5 | | ssel 3914 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
6 | | pm3.2 470 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐵 → (𝜓 → (𝑥 ∈ 𝐵 ∧ 𝜓))) |
7 | 6 | imim2d 57 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵 → ((𝜑 → 𝜓) → (𝜑 → (𝑥 ∈ 𝐵 ∧ 𝜓)))) |
8 | 5, 7 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → ((𝜑 → 𝜓) → (𝜑 → (𝑥 ∈ 𝐵 ∧ 𝜓))))) |
9 | 8 | a2d 29 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) → (𝑥 ∈ 𝐴 → (𝜑 → (𝑥 ∈ 𝐵 ∧ 𝜓))))) |
10 | 9 | imp4a 423 |
. . . . . . . . 9
⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)))) |
11 | 10 | alimdv 1919 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)))) |
12 | 11 | imp 407 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝐵 ∧ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓))) → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓))) |
13 | 4, 12 | sylan2b 594 |
. . . . . 6
⊢ ((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓))) |
14 | | euimmo 2618 |
. . . . . 6
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)) → (∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) → (∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
16 | | df-eu 2569 |
. . . . . 6
⊢
(∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
17 | 16 | simplbi2 501 |
. . . . 5
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → (∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
18 | 15, 17 | syl9 77 |
. . . 4
⊢ ((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → (∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓) → ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))) |
19 | 18 | imp32 419 |
. . 3
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))) → ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
20 | | df-reu 3072 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
21 | 19, 20 | sylibr 233 |
. 2
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃!𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))) → ∃!𝑥 ∈ 𝐴 𝜑) |
22 | 3, 21 | sylan2b 594 |
1
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) |