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	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐵 } ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sneqrg	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐵 } → 𝐴 = 𝐵 ) )
2		sneq	⊢ ( 𝐴 = 𝐵 → { 𝐴 } = { 𝐵 } )
3	1 2	impbid1	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐵 } ↔ 𝐴 = 𝐵 ) )