Theorem euae

Description: Two ways to express "exactly one thing exists". To paraphrase the statement and explain the label: there Exists a Unique thing if and only if for All x , x Equals some given (and disjoint) y . Both sides are false in set theory, see Theorems neutru and dtru . (Contributed by NM, 5-Apr-2004) State the theorem using truth constant T. . (Revised by BJ, 7-Oct-2022) Reduce axiom dependencies. (Revised by Wolf Lammen, 2-Mar-2023)

	Ref	Expression
Assertion	euae	$$⊢\exists !x\top \leftrightarrow \forall xx=y$$

Proof

Step	Hyp	Ref	Expression
1		extru	$$⊢\exists x\top$$
2	1	biantrur	$$⊢\exists y\forall x\left(\top \to x=y\right)\leftrightarrow \left(\exists x\top \wedge \exists y\forall x\left(\top \to x=y\right)\right)$$
3		hbaev	$$⊢\forall xx=y\to \forall y\forall xx=y$$
4	3	19.8w	$$⊢\forall xx=y\to \exists y\forall xx=y$$
5		hbnaev	$$⊢\neg \forall xx=y\to \forall y\neg \forall xx=y$$
6		alnex	$$⊢\forall y\neg \forall xx=y\leftrightarrow \neg \exists y\forall xx=y$$
7	5 6	sylib	$$⊢\neg \forall xx=y\to \neg \exists y\forall xx=y$$
8	7	con4i	$$⊢\exists y\forall xx=y\to \forall xx=y$$
9	4 8	impbii	$$⊢\forall xx=y\leftrightarrow \exists y\forall xx=y$$
10		trut	$$⊢x=y\leftrightarrow \left(\top \to x=y\right)$$
11	10	albii	$$⊢\forall xx=y\leftrightarrow \forall x\left(\top \to x=y\right)$$
12	11	exbii	$$⊢\exists y\forall xx=y\leftrightarrow \exists y\forall x\left(\top \to x=y\right)$$
13	9 12	bitri	$$⊢\forall xx=y\leftrightarrow \exists y\forall x\left(\top \to x=y\right)$$
14		eu3v	$$⊢\exists !x\top \leftrightarrow \left(\exists x\top \wedge \exists y\forall x\left(\top \to x=y\right)\right)$$
15	2 13 14	3bitr4ri	$$⊢\exists !x\top \leftrightarrow \forall xx=y$$