Proof of Theorem reupick
Step | Hyp | Ref
| Expression |
1 | | ssel 3267 |
. . 3
⊢ (A ⊆ B → (x
∈ A
→ x ∈ B)) |
2 | 1 | ad2antrr 706 |
. 2
⊢ (((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) ∧ φ) → (x ∈ A → x ∈ B)) |
3 | | df-rex 2620 |
. . . . . 6
⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ)) |
4 | | df-reu 2621 |
. . . . . 6
⊢ (∃!x ∈ B φ ↔ ∃!x(x ∈ B ∧ φ)) |
5 | 3, 4 | anbi12i 678 |
. . . . 5
⊢ ((∃x ∈ A φ ∧ ∃!x ∈ B φ) ↔ (∃x(x ∈ A ∧ φ) ∧ ∃!x(x ∈ B ∧ φ))) |
6 | 1 | ancrd 537 |
. . . . . . . . . . 11
⊢ (A ⊆ B → (x
∈ A
→ (x ∈ B ∧ x ∈ A))) |
7 | 6 | anim1d 547 |
. . . . . . . . . 10
⊢ (A ⊆ B → ((x
∈ A ∧ φ) →
((x ∈
B ∧
x ∈
A) ∧ φ))) |
8 | | an32 773 |
. . . . . . . . . 10
⊢ (((x ∈ B ∧ x ∈ A) ∧ φ) ↔ ((x ∈ B ∧ φ) ∧
x ∈
A)) |
9 | 7, 8 | syl6ib 217 |
. . . . . . . . 9
⊢ (A ⊆ B → ((x
∈ A ∧ φ) →
((x ∈
B ∧ φ) ∧
x ∈
A))) |
10 | 9 | eximdv 1622 |
. . . . . . . 8
⊢ (A ⊆ B → (∃x(x ∈ A ∧ φ) → ∃x((x ∈ B ∧ φ) ∧
x ∈
A))) |
11 | | eupick 2267 |
. . . . . . . . 9
⊢ ((∃!x(x ∈ B ∧ φ) ∧ ∃x((x ∈ B ∧ φ) ∧
x ∈
A)) → ((x ∈ B ∧ φ) → x ∈ A)) |
12 | 11 | ex 423 |
. . . . . . . 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 422 |
. . . . 5
⊢ ((A ⊆ B ∧ (∃x(x ∈ A ∧ φ) ∧ ∃!x(x ∈ B ∧ φ))) → ((x ∈ B ∧ φ) → x ∈ A)) |
16 | 5, 15 | sylan2b 461 |
. . . 4
⊢ ((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) → ((x ∈ B ∧ φ) → x ∈ A)) |
17 | 16 | exp3acom23 1372 |
. . 3
⊢ ((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) → (φ → (x ∈ B → x ∈ A))) |
18 | 17 | imp 418 |
. 2
⊢ (((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) ∧ φ) → (x ∈ B → x ∈ A)) |
19 | 2, 18 | impbid 183 |
1
⊢ (((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) ∧ φ) → (x ∈ A ↔ x ∈ B)) |