Metamath Proof Explorer

Theorem eqreu

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

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

Proof

Step Hyp Ref Expression
1 eqreu.1 ⊢ x = B → φ ↔ ψ
2 ralbiim ⊢ ∀ x ∈ A φ ↔ x = B ↔ ∀ x ∈ A φ → x = B ∧ ∀ x ∈ A x = B → φ
3 1 ceqsralv ⊢ B ∈ A → ∀ x ∈ A x = B → φ ↔ ψ
4 3 anbi2d ⊢ B ∈ A → ∀ x ∈ A φ → x = B ∧ ∀ x ∈ A x = B → φ ↔ ∀ x ∈ A φ → x = B ∧ ψ
5 2 4 bitrid ⊢ B ∈ A → ∀ x ∈ A φ ↔ x = B ↔ ∀ x ∈ A φ → x = B ∧ ψ
6 reu6i ⊢ B ∈ A ∧ ∀ x ∈ A φ ↔ x = B → ∃! x ∈ A φ
7 6 ex ⊢ B ∈ A → ∀ x ∈ A φ ↔ x = B → ∃! x ∈ A φ
8 5 7 sylbird ⊢ B ∈ A → ∀ x ∈ A φ → x = B ∧ ψ → ∃! x ∈ A φ
9 8 3impib ⊢ B ∈ A ∧ ∀ x ∈ A φ → x = B ∧ ψ → ∃! x ∈ A φ
10 9 3com23 ⊢ B ∈ A ∧ ψ ∧ ∀ x ∈ A φ → x = B → ∃! x ∈ A φ