Theorem eqsnd

Description: Deduce that a set is a singleton. (Contributed by Thierry Arnoux, 10-May-2023)

	Ref	Expression
Hypotheses	eqsnd.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = 𝐵 )
	eqsnd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
Assertion	eqsnd	⊢ ( 𝜑 → 𝐴 = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		eqsnd.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = 𝐵 )
2		eqsnd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
4	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ 𝐴 )
5	3 4	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝐴 )
6	1 5	impbida	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 = 𝐵 ) )
7		velsn	⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
8	6 7	bitr4di	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝐵 } ) )
9	8	eqrdv	⊢ ( 𝜑 → 𝐴 = { 𝐵 } )