This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reupick2

Description: Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reupick2 ⊢ ∀ x ∈ A ψ → φ ∧ ∃ x ∈ A ψ ∧ ∃! x ∈ A φ ∧ x ∈ A → φ ↔ ψ

Proof

Step Hyp Ref Expression
1 ancr ⊢ ψ → φ → ψ → φ ∧ ψ
2 1 ralimi ⊢ ∀ x ∈ A ψ → φ → ∀ x ∈ A ψ → φ ∧ ψ
3 rexim ⊢ ∀ x ∈ A ψ → φ ∧ ψ → ∃ x ∈ A ψ → ∃ x ∈ A φ ∧ ψ
4 2 3 syl ⊢ ∀ x ∈ A ψ → φ → ∃ x ∈ A ψ → ∃ x ∈ A φ ∧ ψ
5 reupick3 ⊢ ∃! x ∈ A φ ∧ ∃ x ∈ A φ ∧ ψ ∧ x ∈ A → φ → ψ
6 5 3exp ⊢ ∃! x ∈ A φ → ∃ x ∈ A φ ∧ ψ → x ∈ A → φ → ψ
7 6 com12 ⊢ ∃ x ∈ A φ ∧ ψ → ∃! x ∈ A φ → x ∈ A → φ → ψ
8 4 7 syl6 ⊢ ∀ x ∈ A ψ → φ → ∃ x ∈ A ψ → ∃! x ∈ A φ → x ∈ A → φ → ψ
9 8 3imp1 ⊢ ∀ x ∈ A ψ → φ ∧ ∃ x ∈ A ψ ∧ ∃! x ∈ A φ ∧ x ∈ A → φ → ψ
10 rsp ⊢ ∀ x ∈ A ψ → φ → x ∈ A → ψ → φ
11 10 3ad2ant1 ⊢ ∀ x ∈ A ψ → φ ∧ ∃ x ∈ A ψ ∧ ∃! x ∈ A φ → x ∈ A → ψ → φ
12 11 imp ⊢ ∀ x ∈ A ψ → φ ∧ ∃ x ∈ A ψ ∧ ∃! x ∈ A φ ∧ x ∈ A → ψ → φ
13 9 12 impbid ⊢ ∀ x ∈ A ψ → φ ∧ ∃ x ∈ A ψ ∧ ∃! x ∈ A φ ∧ x ∈ A → φ ↔ ψ