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

Proof

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

Metamath Proof Explorer

Theorem euae

Proof