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\in V\to \left(\left\{A\right\}=\left\{B\right\}\to A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
2		eleq2	$$⊢\left\{A\right\}=\left\{B\right\}\to \left(A\in \left\{A\right\}\leftrightarrow A\in \left\{B\right\}\right)$$
3	1 2	syl5ibcom	$$⊢A\in V\to \left(\left\{A\right\}=\left\{B\right\}\to A\in \left\{B\right\}\right)$$
4		elsng	$$⊢A\in V\to \left(A\in \left\{B\right\}\leftrightarrow A=B\right)$$
5	3 4	sylibd	$$⊢A\in V\to \left(\left\{A\right\}=\left\{B\right\}\to A=B\right)$$