mosneq

Description: There exists at most one set whose singleton is equal to a given class. See also moeq . (Contributed by BJ, 24-Sep-2022)

		Ref	Expression
	Assertion	mosneq	$⊢ \exists^{*} x \{x\} = A$

Step	Hyp	Ref	Expression
1		eqtr3	$⊢ (\{x\} = A \land \{y\} = A) \to \{x\} = \{y\}$
2		vex	$⊢ x \in V$
3	2	sneqr	$⊢ \{x\} = \{y\} \to x = y$
4	1 3	syl	$⊢ (\{x\} = A \land \{y\} = A) \to x = y$
5	4	gen2	$⊢ \forall x \forall y ((\{x\} = A \land \{y\} = A) \to x = y)$
6		sneq	$⊢ x = y \to \{x\} = \{y\}$
7	6	eqeq1d	$⊢ x = y \to (\{x\} = A \leftrightarrow \{y\} = A)$
8	7	mo4	$⊢ \exists^{*} x \{x\} = A \leftrightarrow \forall x \forall y ((\{x\} = A \land \{y\} = A) \to x = y)$
9	5 8	mpbir	$⊢ \exists^{*} x \{x\} = A$

Metamath Proof Explorer