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

Metamath Proof Explorer

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 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃ 𝑧 𝐴 = { 𝑧 } )