Theorem brsingle

Description: The binary relation form of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brsingle.1	$$⊢A\in \mathrm{V}$$
	brsingle.2	$$⊢B\in \mathrm{V}$$
Assertion	brsingle	$$⊢A\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}B\leftrightarrow B=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		brsingle.1	$$⊢A\in \mathrm{V}$$
2		brsingle.2	$$⊢B\in \mathrm{V}$$
3		df-singleton	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$$
4		brxp	$$⊢A\left(\mathrm{V}\times \mathrm{V}\right)B\leftrightarrow \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
5	1 2 4	mpbir2an	$$⊢A\left(\mathrm{V}\times \mathrm{V}\right)B$$
6		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
7	1	ideq	$$⊢x\mathrm{I}A\leftrightarrow x=A$$
8	6 7	bitr4i	$$⊢x\in \left\{A\right\}\leftrightarrow x\mathrm{I}A$$
9	1 2 3 5 8	brtxpsd3	$$⊢A\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}B\leftrightarrow B=\left\{A\right\}$$