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

Metamath Proof Explorer

Theorem eqeu

Description: A condition which implies existential uniqueness. (Contributed by Jeff Hankins, 8-Sep-2009)

Ref Expression
Hypothesis eqeu.1 ⊢ x = A → φ ↔ ψ
Assertion eqeu ⊢ A ∈ B ∧ ψ ∧ ∀ x φ → x = A → ∃! x φ

Proof

Step Hyp Ref Expression
1 eqeu.1 ⊢ x = A → φ ↔ ψ
2 1 spcegv ⊢ A ∈ B → ψ → ∃ x φ
3 2 imp ⊢ A ∈ B ∧ ψ → ∃ x φ
4 3 3adant3 ⊢ A ∈ B ∧ ψ ∧ ∀ x φ → x = A → ∃ x φ
5 eqeq2 ⊢ y = A → x = y ↔ x = A
6 5 imbi2d ⊢ y = A → φ → x = y ↔ φ → x = A
7 6 albidv ⊢ y = A → ∀ x φ → x = y ↔ ∀ x φ → x = A
8 7 spcegv ⊢ A ∈ B → ∀ x φ → x = A → ∃ y ∀ x φ → x = y
9 8 imp ⊢ A ∈ B ∧ ∀ x φ → x = A → ∃ y ∀ x φ → x = y
10 9 3adant2 ⊢ A ∈ B ∧ ψ ∧ ∀ x φ → x = A → ∃ y ∀ x φ → x = y
11 eu3v ⊢ ∃! x φ ↔ ∃ x φ ∧ ∃ y ∀ x φ → x = y
12 4 10 11 sylanbrc ⊢ A ∈ B ∧ ψ ∧ ∀ x φ → x = A → ∃! x φ