Proof of Theorem reupick
Step | Hyp | Ref
| Expression |
1 | | ssel 2933 |
. . 3
⊢ (A ⊆ B
→ (x ∈ A →
x ∈
B)) |
2 | 1 | ad2antrr 457 |
. 2
⊢
(((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) ∧ φ) → (x ∈ A → x ∈ B)) |
3 | | df-rex 2306 |
. . . . . 6
⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ)) |
4 | | df-reu 2307 |
. . . . . 6
⊢ (∃!x ∈ B φ ↔ ∃!x(x ∈ B ∧ φ)) |
5 | 3, 4 | anbi12i 433 |
. . . . 5
⊢ ((∃x ∈ A φ ∧ ∃!x ∈ B φ) ↔ (∃x(x ∈ A ∧ φ) ∧ ∃!x(x ∈ B ∧ φ))) |
6 | 1 | ancrd 309 |
. . . . . . . . . . 11
⊢ (A ⊆ B
→ (x ∈ A →
(x ∈
B ∧
x ∈
A))) |
7 | 6 | anim1d 319 |
. . . . . . . . . 10
⊢ (A ⊆ B
→ ((x ∈ A ∧ φ) →
((x ∈
B ∧
x ∈
A) ∧ φ))) |
8 | | an32 496 |
. . . . . . . . . 10
⊢
(((x ∈ B ∧ x ∈ A) ∧ φ) ↔
((x ∈
B ∧ φ) ∧
x ∈
A)) |
9 | 7, 8 | syl6ib 150 |
. . . . . . . . 9
⊢ (A ⊆ B
→ ((x ∈ A ∧ φ) →
((x ∈
B ∧ φ) ∧
x ∈
A))) |
10 | 9 | eximdv 1757 |
. . . . . . . 8
⊢ (A ⊆ B
→ (∃x(x ∈ A ∧ φ) →
∃x((x ∈ B ∧ φ) ∧ x ∈ A))) |
11 | | eupick 1976 |
. . . . . . . . 9
⊢ ((∃!x(x ∈ B ∧ φ) ∧ ∃x((x ∈ B ∧ φ) ∧
x ∈
A)) → ((x ∈ B ∧ φ) → x ∈ A)) |
12 | 11 | ex 108 |
. . . . . . . 8
⊢ (∃!x(x ∈ B ∧ φ) → (∃x((x ∈ B ∧ φ) ∧
x ∈
A) → ((x ∈ B ∧ φ) → x ∈ A))) |
13 | 10, 12 | syl9 66 |
. . . . . . 7
⊢ (A ⊆ B
→ (∃!x(x ∈ B ∧ φ) →
(∃x(x ∈ A ∧ φ) →
((x ∈
B ∧ φ) → x ∈ A)))) |
14 | 13 | com23 72 |
. . . . . 6
⊢ (A ⊆ B
→ (∃x(x ∈ A ∧ φ) →
(∃!x(x ∈ B ∧ φ) →
((x ∈
B ∧ φ) → x ∈ A)))) |
15 | 14 | imp32 244 |
. . . . 5
⊢
((A ⊆ B ∧ (∃x(x ∈ A ∧ φ) ∧ ∃!x(x ∈ B ∧ φ))) → ((x ∈ B ∧ φ) → x ∈ A)) |
16 | 5, 15 | sylan2b 271 |
. . . 4
⊢
((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) → ((x ∈ B ∧ φ) → x ∈ A)) |
17 | 16 | expcomd 1327 |
. . 3
⊢
((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) → (φ → (x ∈ B → x ∈ A))) |
18 | 17 | imp 115 |
. 2
⊢
(((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) ∧ φ) → (x ∈ B → x ∈ A)) |
19 | 2, 18 | impbid 120 |
1
⊢
(((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) ∧ φ) → (x ∈ A ↔ x ∈ B)) |