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	3	elsnd	$$⊢\left(x\in A\wedge y\in \left\{x\right\}\right)\to y=x$$
5	4	equcomd	$$⊢\left(x\in A\wedge y\in \left\{x\right\}\right)\to x=y$$
6	5	moimi	$$⊢{\exists }^{*}xx=y\to {\exists }^{*}x\left(x\in A\wedge y\in \left\{x\right\}\right)$$
7	2 6	ax-mp	$$⊢{\exists }^{*}x\left(x\in A\wedge y\in \left\{x\right\}\right)$$
8	1 7	mpgbir	$$⊢\underset{x\in A}{Disj}\left\{x\right\}$$