Theorem wl-moae

Description: Two ways to express "at most one thing exists" or, in this context equivalently, "exactly one thing exists" . The equivalence results from the presence of ax-6 in the proof, that ensures "at least one thing exists". For other equivalences see wl-euae and exists1 . Gerard Lang pointed out, that E. y A. x x = y with disjoint x and y ( dfmo , trut ) also means "exactly one thing exists" . (Contributed by NM, 5-Apr-2004) State the theorem using truth constant T. . (Revised by BJ, 7-Oct-2022) Reduce axiom dependencies, and use E* . (Revised by Wolf Lammen, 7-Mar-2023)

	Ref	Expression
Assertion	wl-moae	$$⊢{\exists }^{*}x\top \leftrightarrow \forall xx=y$$

Proof

Step	Hyp	Ref	Expression
1		wl-motae	$$⊢{\exists }^{*}x\top \to \forall xx=y$$
2		hbaev	$$⊢\forall xx=y\to \forall y\forall xx=y$$
3	2	19.8w	$$⊢\forall xx=y\to \exists y\forall xx=y$$
4		ax-1	$$⊢x=y\to \left(\top \to x=y\right)$$
5	4	alimi	$$⊢\forall xx=y\to \forall x\left(\top \to x=y\right)$$
6	5	eximi	$$⊢\exists y\forall xx=y\to \exists y\forall x\left(\top \to x=y\right)$$
7	3 6	syl	$$⊢\forall xx=y\to \exists y\forall x\left(\top \to x=y\right)$$
8		dfmo	$$⊢{\exists }^{*}x\top \leftrightarrow \exists y\forall x\left(\top \to x=y\right)$$
9	7 8	sylibr	$$⊢\forall xx=y\to {\exists }^{*}x\top$$
10	1 9	impbii	$$⊢{\exists }^{*}x\top \leftrightarrow \forall xx=y$$