sndisj

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

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

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

Metamath Proof Explorer