Theorem fvsingle

Description: The value of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Revised by Scott Fenton, 13-Apr-2018)

	Ref	Expression
Assertion	fvsingle	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(A\right)=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢x=A\to \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(x\right)=\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(A\right)$$
2		sneq	$$⊢x=A\to \left\{x\right\}=\left\{A\right\}$$
3	1 2	eqeq12d	$$⊢x=A\to \left(\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(x\right)=\left\{x\right\}\leftrightarrow \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(A\right)=\left\{A\right\}\right)$$
4		eqid	$$⊢\left\{x\right\}=\left\{x\right\}$$
5		vex	$$⊢x\in \mathrm{V}$$
6		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
7	5 6	brsingle	$$⊢x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{x\right\}\leftrightarrow \left\{x\right\}=\left\{x\right\}$$
8	4 7	mpbir	$$⊢x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{x\right\}$$
9		fnsingle	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}Fn\mathrm{V}$$
10		fnbrfvb	$$⊢\left(\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}Fn\mathrm{V}\wedge x\in \mathrm{V}\right)\to \left(\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(x\right)=\left\{x\right\}\leftrightarrow x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{x\right\}\right)$$
11	9 5 10	mp2an	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(x\right)=\left\{x\right\}\leftrightarrow x\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left\{x\right\}$$
12	8 11	mpbir	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(x\right)=\left\{x\right\}$$
13	3 12	vtoclg	$$⊢A\in \mathrm{V}\to \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(A\right)=\left\{A\right\}$$
14		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(A\right)=\varnothing$$
15		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
16	15	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
17	14 16	eqtr4d	$$⊢\neg A\in \mathrm{V}\to \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(A\right)=\left\{A\right\}$$
18	13 17	pm2.61i	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\left(A\right)=\left\{A\right\}$$