Theorem elsingles

Description: Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Assertion	elsingles	$$⊢A\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\leftrightarrow \exists xA=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\to A\in \mathrm{V}$$
2		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
3		eleq1	$$⊢A=\left\{x\right\}\to \left(A\in \mathrm{V}\leftrightarrow \left\{x\right\}\in \mathrm{V}\right)$$
4	2 3	mpbiri	$$⊢A=\left\{x\right\}\to A\in \mathrm{V}$$
5	4	exlimiv	$$⊢\exists xA=\left\{x\right\}\to A\in \mathrm{V}$$
6		eleq1	$$⊢y=A\to \left(y\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\leftrightarrow A\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)$$
7		eqeq1	$$⊢y=A\to \left(y=\left\{x\right\}\leftrightarrow A=\left\{x\right\}\right)$$
8	7	exbidv	$$⊢y=A\to \left(\exists xy=\left\{x\right\}\leftrightarrow \exists xA=\left\{x\right\}\right)$$
9		df-singles	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}=\mathrm{ran}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
10	9	eleq2i	$$⊢y\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\leftrightarrow y\in \mathrm{ran}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
11		vex	$$⊢y\in \mathrm{V}$$
12	11	elrn	$$⊢y\in \mathrm{ran}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\leftrightarrow \exists xx\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y$$
13		vex	$$⊢x\in \mathrm{V}$$
14	13 11	brsingle	$$⊢x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y\leftrightarrow y=\left\{x\right\}$$
15	14	exbii	$$⊢\exists xx\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}y\leftrightarrow \exists xy=\left\{x\right\}$$
16	10 12 15	3bitri	$$⊢y\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\leftrightarrow \exists xy=\left\{x\right\}$$
17	6 8 16	vtoclbg	$$⊢A\in \mathrm{V}\to \left(A\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\leftrightarrow \exists xA=\left\{x\right\}\right)$$
18	1 5 17	pm5.21nii	$$⊢A\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\leftrightarrow \exists xA=\left\{x\right\}$$