Theorem snssg

Description: The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of Quine p. 49. (Contributed by NM, 22-Jul-2001) (Proof shortened by BJ, 1-Jan-2025)

	Ref	Expression
Assertion	snssg	$$⊢A\in V\to \left(A\in B\leftrightarrow \left\{A\right\}\subseteq B\right)$$

Proof

Step	Hyp	Ref	Expression
1		snssb	$$⊢\left\{A\right\}\subseteq B\leftrightarrow \left(A\in \mathrm{V}\to A\in B\right)$$
2	1	bicomi	$$⊢\left(A\in \mathrm{V}\to A\in B\right)\leftrightarrow \left\{A\right\}\subseteq B$$
3		elex	$$⊢A\in V\to A\in \mathrm{V}$$
4		imbibi	$$⊢\left(\left(A\in \mathrm{V}\to A\in B\right)\leftrightarrow \left\{A\right\}\subseteq B\right)\to \left(A\in \mathrm{V}\to \left(A\in B\leftrightarrow \left\{A\right\}\subseteq B\right)\right)$$
5	2 3 4	mpsyl	$$⊢A\in V\to \left(A\in B\leftrightarrow \left\{A\right\}\subseteq B\right)$$