Theorem issn

Description: A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020)

	Ref	Expression
Assertion	issn	⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃ 𝑧 𝐴 = { 𝑧 } )

Proof

Step	Hyp	Ref	Expression
1		equcom	⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
2	1	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 ) )
3	2	ralbidv	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 = 𝑥 ) )
4		ne0i	⊢ ( 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅ )
5		eqsn	⊢ ( 𝐴 ≠ ∅ → ( 𝐴 = { 𝑥 } ↔ ∀ 𝑦 ∈ 𝐴 𝑦 = 𝑥 ) )
6	4 5	syl	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 = { 𝑥 } ↔ ∀ 𝑦 ∈ 𝐴 𝑦 = 𝑥 ) )
7	3 6	bitr4d	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ↔ 𝐴 = { 𝑥 } ) )
8		sneq	⊢ ( 𝑧 = 𝑥 → { 𝑧 } = { 𝑥 } )
9	8	eqeq2d	⊢ ( 𝑧 = 𝑥 → ( 𝐴 = { 𝑧 } ↔ 𝐴 = { 𝑥 } ) )
10	9	spcegv	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 = { 𝑥 } → ∃ 𝑧 𝐴 = { 𝑧 } ) )
11	7 10	sylbid	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃ 𝑧 𝐴 = { 𝑧 } ) )
12	11	rexlimiv	⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃ 𝑧 𝐴 = { 𝑧 } )