Metamath Proof Explorer

Theorem sneqrg

Description: Closed form of sneqr . (Contributed by Scott Fenton, 1-Apr-2011) (Proof shortened by JJ, 23-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 snidg 
 |-  ( A e. V -> A e. { A } )
2 eleq2 
 |-  ( { A } = { B } -> ( A e. { A } <-> A e. { B } ) )
3 1 2 syl5ibcom 
 |-  ( A e. V -> ( { A } = { B } -> A e. { B } ) )
4 elsng 
 |-  ( A e. V -> ( A e. { B } <-> A = B ) )
5 3 4 sylibd 
 |-  ( A e. V -> ( { A } = { B } -> A = B ) )