Theorem issn

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

	Ref	Expression
Assertion	issn	$$⊢\exists x\in A\forall y\in Ax=y\to \exists zA=\left\{z\right\}$$

Proof

Step	Hyp	Ref	Expression
1		equcom	$$⊢x=y\leftrightarrow y=x$$
2	1	a1i	$$⊢x\in A\to \left(x=y\leftrightarrow y=x\right)$$
3	2	ralbidv	$$⊢x\in A\to \left(\forall y\in Ax=y\leftrightarrow \forall y\in Ay=x\right)$$
4		ne0i	$$⊢x\in A\to A\ne \varnothing$$
5		eqsn	$$⊢A\ne \varnothing \to \left(A=\left\{x\right\}\leftrightarrow \forall y\in Ay=x\right)$$
6	4 5	syl	$$⊢x\in A\to \left(A=\left\{x\right\}\leftrightarrow \forall y\in Ay=x\right)$$
7	3 6	bitr4d	$$⊢x\in A\to \left(\forall y\in Ax=y\leftrightarrow A=\left\{x\right\}\right)$$
8		sneq	$$⊢z=x\to \left\{z\right\}=\left\{x\right\}$$
9	8	eqeq2d	$$⊢z=x\to \left(A=\left\{z\right\}\leftrightarrow A=\left\{x\right\}\right)$$
10	9	spcegv	$$⊢x\in A\to \left(A=\left\{x\right\}\to \exists zA=\left\{z\right\}\right)$$
11	7 10	sylbid	$$⊢x\in A\to \left(\forall y\in Ax=y\to \exists zA=\left\{z\right\}\right)$$
12	11	rexlimiv	$$⊢\exists x\in A\forall y\in Ax=y\to \exists zA=\left\{z\right\}$$