This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjxsn

Description: A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

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

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