wl-euae

Description: Two ways to express "exactly one thing exists" . (Contributed by Wolf Lammen, 5-Mar-2023)

		Ref	Expression
	Assertion	wl-euae	$⊢ \exists! x ⊤ \leftrightarrow \forall x x = y$

Step	Hyp	Ref	Expression
1		df-eu	$⊢ \exists! x ⊤ \leftrightarrow (\exists x ⊤ \land \exists^{*} x ⊤)$
2		extru	$⊢ \exists x ⊤$
3	2	biantrur	$⊢ \exists^{} x ⊤ \leftrightarrow (\exists x ⊤ \land \exists^{} x ⊤)$
4		wl-moae	$⊢ \exists^{*} x ⊤ \leftrightarrow \forall x x = y$
5	1 3 4	3bitr2i	$⊢ \exists! x ⊤ \leftrightarrow \forall x x = y$

Metamath Proof Explorer