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

Proof

Step	Hyp	Ref	Expression
1		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
2		eleq2	⊢ ( { 𝐴 } = { 𝐵 } → ( 𝐴 ∈ { 𝐴 } ↔ 𝐴 ∈ { 𝐵 } ) )
3	1 2	syl5ibcom	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐵 } → 𝐴 ∈ { 𝐵 } ) )
4		elsng	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) )
5	3 4	sylibd	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐵 } → 𝐴 = 𝐵 ) )