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 A x = y \to \exists z A = \{z\}$

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

Metamath Proof Explorer