This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exists1

Description: Two ways to express "exactly one thing exists". The left-hand side requires only one variable to express this. Both sides are false in set theory, see Theorem dtru . (Contributed by NM, 5-Apr-2004) (Proof shortened by BJ, 7-Oct-2022)

		Ref	Expression
	Assertion	exists1	$⊢ \exists! x x = x \leftrightarrow \forall x x = y$

Proof

Step	Hyp	Ref	Expression
1		equid	$⊢ x = x$
2	1	bitru	$⊢ x = x \leftrightarrow ⊤$
3	2	eubii	$⊢ \exists! x x = x \leftrightarrow \exists! x ⊤$
4		euae	$⊢ \exists! x ⊤ \leftrightarrow \forall x x = y$
5	3 4	bitri	$⊢ \exists! x x = x \leftrightarrow \forall x x = y$