This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )