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 } )