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}\varnothing$$

Proof

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