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 AVA=BA=B

Proof

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