Theorem eqsn

Description: Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007) (Proof shortened by JJ, 23-Jul-2021)

	Ref	Expression
Assertion	eqsn	⊢ ( 𝐴 ≠ ∅ → ( 𝐴 = { 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ne	⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
2		biorf	⊢ ( ¬ 𝐴 = ∅ → ( 𝐴 = { 𝐵 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ) )
3	1 2	sylbi	⊢ ( 𝐴 ≠ ∅ → ( 𝐴 = { 𝐵 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ) )
4		dfss3	⊢ ( 𝐴 ⊆ { 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { 𝐵 } )
5		sssn	⊢ ( 𝐴 ⊆ { 𝐵 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) )
6		velsn	⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
7	6	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = 𝐵 )
8	4 5 7	3bitr3i	⊢ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = 𝐵 )
9	3 8	bitrdi	⊢ ( 𝐴 ≠ ∅ → ( 𝐴 = { 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = 𝐵 ) )