Theorem snsssng

Description: If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006) (Revised by Thierry Arnoux, 11-Apr-2024)

	Ref	Expression
Assertion	snsssng	$$⊢\left(A\in V\wedge \left\{A\right\}\subseteq \left\{B\right\}\right)\to A=B$$

Proof

Step	Hyp	Ref	Expression
1		sssn	$$⊢\left\{A\right\}\subseteq \left\{B\right\}\leftrightarrow \left(\left\{A\right\}=\varnothing \vee \left\{A\right\}=\left\{B\right\}\right)$$
2		snnzg	$$⊢A\in V\to \left\{A\right\}\ne \varnothing$$
3	2	neneqd	$$⊢A\in V\to \neg \left\{A\right\}=\varnothing$$
4	3	pm2.21d	$$⊢A\in V\to \left(\left\{A\right\}=\varnothing \to A=B\right)$$
5		sneqrg	$$⊢A\in V\to \left(\left\{A\right\}=\left\{B\right\}\to A=B\right)$$
6	4 5	jaod	$$⊢A\in V\to \left(\left(\left\{A\right\}=\varnothing \vee \left\{A\right\}=\left\{B\right\}\right)\to A=B\right)$$
7	6	imp	$$⊢\left(A\in V\wedge \left(\left\{A\right\}=\varnothing \vee \left\{A\right\}=\left\{B\right\}\right)\right)\to A=B$$
8	1 7	sylan2b	$$⊢\left(A\in V\wedge \left\{A\right\}\subseteq \left\{B\right\}\right)\to A=B$$