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

Metamath Proof Explorer

Theorem reu6i

Description: A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Assertion reu6i ⊢ B ∈ A ∧ ∀ x ∈ A φ ↔ x = B → ∃! x ∈ A φ

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ y = B → x = y ↔ x = B
2 1 bibi2d ⊢ y = B → φ ↔ x = y ↔ φ ↔ x = B
3 2 ralbidv ⊢ y = B → ∀ x ∈ A φ ↔ x = y ↔ ∀ x ∈ A φ ↔ x = B
4 3 rspcev ⊢ B ∈ A ∧ ∀ x ∈ A φ ↔ x = B → ∃ y ∈ A ∀ x ∈ A φ ↔ x = y
5 reu6 ⊢ ∃! x ∈ A φ ↔ ∃ y ∈ A ∀ x ∈ A φ ↔ x = y
6 4 5 sylibr ⊢ B ∈ A ∧ ∀ x ∈ A φ ↔ x = B → ∃! x ∈ A φ