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 ( df-mo , 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	|- ( E* x T. <-> A. x x = y )

Proof

Step	Hyp	Ref	Expression
1		wl-motae	|- ( E* x T. -> A. x x = y )
2		hbaev	|- ( A. x x = y -> A. y A. x x = y )
3	2	19.8w	|- ( A. x x = y -> E. y A. x x = y )
4		ax-1	|- ( x = y -> ( T. -> x = y ) )
5	4	alimi	|- ( A. x x = y -> A. x ( T. -> x = y ) )
6	5	eximi	|- ( E. y A. x x = y -> E. y A. x ( T. -> x = y ) )
7	3 6	syl	|- ( A. x x = y -> E. y A. x ( T. -> x = y ) )
8		df-mo	|- ( E* x T. <-> E. y A. x ( T. -> x = y ) )
9	7 8	sylibr	|- ( A. x x = y -> E* x T. )
10	1 9	impbii	|- ( E* x T. <-> A. x x = y )