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 !xx=x\leftrightarrow \forall xx=y$$

Proof

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