Theorem int0el

Description: The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	int0el	$$⊢\varnothing \in A\to \bigcap A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		intss1	$$⊢\varnothing \in A\to \bigcap A\subseteq \varnothing$$
2		0ss	$$⊢\varnothing \subseteq \bigcap A$$
3	2	a1i	$$⊢\varnothing \in A\to \varnothing \subseteq \bigcap A$$
4	1 3	eqssd	$$⊢\varnothing \in A\to \bigcap A=\varnothing$$