Metamath Proof Explorer

Theorem reupick

Description: Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999)

Ref Expression
Assertion reupick ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ ∧ φ → x ∈ A ↔ x ∈ B

Proof

Step Hyp Ref Expression
1 ssel ⊢ A ⊆ B → x ∈ A → x ∈ B
2 1 ad2antrr ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ ∧ φ → x ∈ A → x ∈ B
3 df-rex ⊢ ∃ x ∈ A φ ↔ ∃ x x ∈ A ∧ φ
4 df-reu ⊢ ∃! x ∈ B φ ↔ ∃! x x ∈ B ∧ φ
5 3 4 anbi12i ⊢ ∃ x ∈ A φ ∧ ∃! x ∈ B φ ↔ ∃ x x ∈ A ∧ φ ∧ ∃! x x ∈ B ∧ φ
6 1 ancrd ⊢ A ⊆ B → x ∈ A → x ∈ B ∧ x ∈ A
7 6 anim1d ⊢ A ⊆ B → x ∈ A ∧ φ → x ∈ B ∧ x ∈ A ∧ φ
8 an32 ⊢ x ∈ B ∧ x ∈ A ∧ φ ↔ x ∈ B ∧ φ ∧ x ∈ A
9 7 8 syl6ib ⊢ A ⊆ B → x ∈ A ∧ φ → x ∈ B ∧ φ ∧ x ∈ A
10 9 eximdv ⊢ A ⊆ B → ∃ x x ∈ A ∧ φ → ∃ x x ∈ B ∧ φ ∧ x ∈ A
11 eupick ⊢ ∃! x x ∈ B ∧ φ ∧ ∃ x x ∈ B ∧ φ ∧ x ∈ A → x ∈ B ∧ φ → x ∈ A
12 11 ex ⊢ ∃! x x ∈ B ∧ φ → ∃ x x ∈ B ∧ φ ∧ x ∈ A → x ∈ B ∧ φ → x ∈ A
13 10 12 syl9 ⊢ A ⊆ B → ∃! x x ∈ B ∧ φ → ∃ x x ∈ A ∧ φ → x ∈ B ∧ φ → x ∈ A
14 13 com23 ⊢ A ⊆ B → ∃ x x ∈ A ∧ φ → ∃! x x ∈ B ∧ φ → x ∈ B ∧ φ → x ∈ A
15 14 imp32 ⊢ A ⊆ B ∧ ∃ x x ∈ A ∧ φ ∧ ∃! x x ∈ B ∧ φ → x ∈ B ∧ φ → x ∈ A
16 5 15 sylan2b ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → x ∈ B ∧ φ → x ∈ A
17 16 expcomd ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → φ → x ∈ B → x ∈ A
18 17 imp ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ ∧ φ → x ∈ B → x ∈ A
19 2 18 impbid ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ ∧ φ → x ∈ A ↔ x ∈ B