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

Metamath Proof Explorer

Theorem 0disj

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

		Ref	Expression
	Assertion	0disj	$⊢ \underset{x \in A}{Disj} \emptyset$

Step	Hyp	Ref	Expression
1		0ss	$⊢ \emptyset \subseteq \{x\}$
2	1	rgenw	$⊢ \forall x \in A \emptyset \subseteq \{x\}$
3		sndisj	$⊢ \underset{x \in A}{Disj} \{x\}$
4		disjss2	$⊢ \forall x \in A \emptyset \subseteq \{x\} \to (\underset{x \in A}{Disj} \{x\} \to \underset{x \in A}{Disj} \emptyset)$
5	2 3 4	mp2	$⊢ \underset{x \in A}{Disj} \emptyset$