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 
|- ( E. x e. A A. y e. A x = y -> E. z A = { z } )

Proof

Step Hyp Ref Expression
1 equcom 
 |-  ( x = y <-> y = x )
2 1 a1i 
 |-  ( x e. A -> ( x = y <-> y = x ) )
3 2 ralbidv 
 |-  ( x e. A -> ( A. y e. A x = y <-> A. y e. A y = x ) )
4 ne0i 
 |-  ( x e. A -> A =/= (/) )
5 eqsn 
 |-  ( A =/= (/) -> ( A = { x } <-> A. y e. A y = x ) )
6 4 5 syl 
 |-  ( x e. A -> ( A = { x } <-> A. y e. A y = x ) )
7 3 6 bitr4d 
 |-  ( x e. A -> ( A. y e. A x = y <-> A = { x } ) )
8 sneq 
 |-  ( z = x -> { z } = { x } )
9 8 eqeq2d 
 |-  ( z = x -> ( A = { z } <-> A = { x } ) )
10 9 spcegv 
 |-  ( x e. A -> ( A = { x } -> E. z A = { z } ) )
11 7 10 sylbid 
 |-  ( x e. A -> ( A. y e. A x = y -> E. z A = { z } ) )
12 11 rexlimiv 
 |-  ( E. x e. A A. y e. A x = y -> E. z A = { z } )