Metamath Proof Explorer

Theorem wl-euae

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

Ref Expression
Assertion wl-euae 
|- ( E! x T. <-> A. x x = y )

Proof

Step Hyp Ref Expression
1 df-eu 
 |-  ( E! x T. <-> ( E. x T. /\ E* x T. ) )
2 extru 
 |-  E. x T.
3 2 biantrur 
 |-  ( E* x T. <-> ( E. x T. /\ E* x T. ) )
4 wl-moae 
 |-  ( E* x T. <-> A. x x = y )
5 1 3 4 3bitr2i 
 |-  ( E! x T. <-> A. x x = y )