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

Metamath Proof Explorer

Theorem eqsnd

Description: Deduce that a set is a singleton. (Contributed by Thierry Arnoux, 10-May-2023) (Proof shortened by SN, 3-Jul-2025)

Ref Expression
Hypotheses eqsnd.1 ⊢ φ ∧ x ∈ A → x = B
eqsnd.2 ⊢ φ → B ∈ A
Assertion eqsnd ⊢ φ → A = B

Proof

Step Hyp Ref Expression
1 eqsnd.1 ⊢ φ ∧ x ∈ A → x = B
2 eqsnd.2 ⊢ φ → B ∈ A
3 1 ralrimiva ⊢ φ → ∀ x ∈ A x = B
4 2 ne0d ⊢ φ → A ≠ ∅
5 eqsn ⊢ A ≠ ∅ → A = B ↔ ∀ x ∈ A x = B
6 4 5 syl ⊢ φ → A = B ↔ ∀ x ∈ A x = B
7 3 6 mpbird ⊢ φ → A = B