Metamath Proof Explorer

Theorem sneqbg

Description: Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012)

Ref Expression
Assertion sneqbg 
|- ( A e. V -> ( { A } = { B } <-> A = B ) )

Proof

Step Hyp Ref Expression
1 sneqrg 
 |-  ( A e. V -> ( { A } = { B } -> A = B ) )
2 sneq 
 |-  ( A = B -> { A } = { B } )
3 1 2 impbid1 
 |-  ( A e. V -> ( { A } = { B } <-> A = B ) )