Theorem sndisj

Description: Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	sndisj	$$⊢\underset{x\in A}{Disj}\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfdisj2	$$⊢\underset{x\in A}{Disj}\left\{x\right\}\leftrightarrow \forall y{\exists }^{*}x\left(x\in A\wedge y\in \left\{x\right\}\right)$$
2		moeq	$$⊢{\exists }^{*}xx=y$$
3		simpr	$$⊢\left(x\in A\wedge y\in \left\{x\right\}\right)\to y\in \left\{x\right\}$$
4		velsn	$$⊢y\in \left\{x\right\}\leftrightarrow y=x$$
5	3 4	sylib	$$⊢\left(x\in A\wedge y\in \left\{x\right\}\right)\to y=x$$
6	5	equcomd	$$⊢\left(x\in A\wedge y\in \left\{x\right\}\right)\to x=y$$
7	6	moimi	$$⊢{\exists }^{*}xx=y\to {\exists }^{*}x\left(x\in A\wedge y\in \left\{x\right\}\right)$$
8	2 7	ax-mp	$$⊢{\exists }^{*}x\left(x\in A\wedge y\in \left\{x\right\}\right)$$
9	1 8	mpgbir	$$⊢\underset{x\in A}{Disj}\left\{x\right\}$$