Theorem disjx0

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

	Ref	Expression
Assertion	disjx0	$$⊢\underset{x\in \varnothing }{Disj}B$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq \left\{\varnothing \right\}$$
2		disjxsn	$$⊢\underset{x\in \left\{\varnothing \right\}}{Disj}B$$
3		disjss1	$$⊢\varnothing \subseteq \left\{\varnothing \right\}\to \left(\underset{x\in \left\{\varnothing \right\}}{Disj}B\to \underset{x\in \varnothing }{Disj}B\right)$$
4	1 2 3	mp2	$$⊢\underset{x\in \varnothing }{Disj}B$$