Theorem iin0

Description: An indexed intersection of the empty set, with a nonempty index set, is empty. (Contributed by NM, 20-Oct-2005)

	Ref	Expression
Assertion	iin0	$$⊢A\ne \varnothing \leftrightarrow \bigcap _{x\in A}\varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		iinconst	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\varnothing =\varnothing$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2	n0ii	$$⊢\neg \mathrm{V}=\varnothing$$
4		0iin	$$⊢\bigcap _{x\in \varnothing }\varnothing =\mathrm{V}$$
5	4	eqeq1i	$$⊢\bigcap _{x\in \varnothing }\varnothing =\varnothing \leftrightarrow \mathrm{V}=\varnothing$$
6	3 5	mtbir	$$⊢\neg \bigcap _{x\in \varnothing }\varnothing =\varnothing$$
7		iineq1	$$⊢A=\varnothing \to \bigcap _{x\in A}\varnothing =\bigcap _{x\in \varnothing }\varnothing$$
8	7	eqeq1d	$$⊢A=\varnothing \to \left(\bigcap _{x\in A}\varnothing =\varnothing \leftrightarrow \bigcap _{x\in \varnothing }\varnothing =\varnothing \right)$$
9	6 8	mtbiri	$$⊢A=\varnothing \to \neg \bigcap _{x\in A}\varnothing =\varnothing$$
10	9	necon2ai	$$⊢\bigcap _{x\in A}\varnothing =\varnothing \to A\ne \varnothing$$
11	1 10	impbii	$$⊢A\ne \varnothing \leftrightarrow \bigcap _{x\in A}\varnothing =\varnothing$$