Metamath Proof Explorer


Theorem eusnsn

Description: There is a unique element of a singleton which is equal to another singleton. (Contributed by AV, 24-Aug-2022)

Ref Expression
Assertion eusnsn
|- E! x { x } = { y }

Proof

Step Hyp Ref Expression
1 equequ2
 |-  ( z = y -> ( x = z <-> x = y ) )
2 1 bibi2d
 |-  ( z = y -> ( ( { x } = { y } <-> x = z ) <-> ( { x } = { y } <-> x = y ) ) )
3 2 albidv
 |-  ( z = y -> ( A. x ( { x } = { y } <-> x = z ) <-> A. x ( { x } = { y } <-> x = y ) ) )
4 sneqbg
 |-  ( x e. _V -> ( { x } = { y } <-> x = y ) )
5 4 elv
 |-  ( { x } = { y } <-> x = y )
6 5 ax-gen
 |-  A. x ( { x } = { y } <-> x = y )
7 3 6 speivw
 |-  E. z A. x ( { x } = { y } <-> x = z )
8 eu6
 |-  ( E! x { x } = { y } <-> E. z A. x ( { x } = { y } <-> x = z ) )
9 7 8 mpbir
 |-  E! x { x } = { y }