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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = 𝐵 )
	eqsnd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
Assertion	eqsnd	⊢ ( 𝜑 → 𝐴 = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		eqsnd.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = 𝐵 )
2		eqsnd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3	1	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 = 𝐵 )
4	2	ne0d	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
5		eqsn	⊢ ( 𝐴 ≠ ∅ → ( 𝐴 = { 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = 𝐵 ) )
6	4 5	syl	⊢ ( 𝜑 → ( 𝐴 = { 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = 𝐵 ) )
7	3 6	mpbird	⊢ ( 𝜑 → 𝐴 = { 𝐵 } )