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 V A = B A = B

Proof

Step Hyp Ref Expression
1 sneqrg A V A = B A = B
2 sneq A = B A = B
3 1 2 impbid1 A V A = B A = B