Theorem snelsingles

Description: A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Hypothesis	snelsingles.1	$$⊢A\in \mathrm{V}$$
Assertion	snelsingles	$$⊢\left\{A\right\}\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}$$

Proof

Step	Hyp	Ref	Expression
1		snelsingles.1	$$⊢A\in \mathrm{V}$$
2		isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$
3		eqcom	$$⊢x=A\leftrightarrow A=x$$
4	3	exbii	$$⊢\exists xx=A\leftrightarrow \exists xA=x$$
5	2 4	bitri	$$⊢A\in \mathrm{V}\leftrightarrow \exists xA=x$$
6	1 5	mpbi	$$⊢\exists xA=x$$
7		sneq	$$⊢A=x\to \left\{A\right\}=\left\{x\right\}$$
8	6 7	eximii	$$⊢\exists x\left\{A\right\}=\left\{x\right\}$$
9		elsingles	$$⊢\left\{A\right\}\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\leftrightarrow \exists x\left\{A\right\}=\left\{x\right\}$$
10	8 9	mpbir	$$⊢\left\{A\right\}\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}$$