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	|- ( E! x T. <-> A. x x = y )

Proof

Step	Hyp	Ref	Expression
1		extru	|- E. x T.
2	1	biantrur	|- ( E. y A. x ( T. -> x = y ) <-> ( E. x T. /\ E. y A. x ( T. -> x = y ) ) )
3		hbaev	|- ( A. x x = y -> A. y A. x x = y )
4	3	19.8w	|- ( A. x x = y -> E. y A. x x = y )
5		hbnaev	|- ( -. A. x x = y -> A. y -. A. x x = y )
6		alnex	|- ( A. y -. A. x x = y <-> -. E. y A. x x = y )
7	5 6	sylib	|- ( -. A. x x = y -> -. E. y A. x x = y )
8	7	con4i	|- ( E. y A. x x = y -> A. x x = y )
9	4 8	impbii	|- ( A. x x = y <-> E. y A. x x = y )
10		trut	|- ( x = y <-> ( T. -> x = y ) )
11	10	albii	|- ( A. x x = y <-> A. x ( T. -> x = y ) )
12	11	exbii	|- ( E. y A. x x = y <-> E. y A. x ( T. -> x = y ) )
13	9 12	bitri	|- ( A. x x = y <-> E. y A. x ( T. -> x = y ) )
14		eu3v	|- ( E! x T. <-> ( E. x T. /\ E. y A. x ( T. -> x = y ) ) )
15	2 13 14	3bitr4ri	|- ( E! x T. <-> A. x x = y )