Theorem iineq0

Description: An indexed intersection is empty if one of the intersected classes is empty. (Contributed by Zhi Wang, 30-Oct-2025)

	Ref	Expression
Assertion	iineq0	$$⊢\exists x\in AB=\varnothing \to \bigcap _{x\in A}B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nel02	$$⊢B=\varnothing \to \neg y\in B$$
2	1	reximi	$$⊢\exists x\in AB=\varnothing \to \exists x\in A\neg y\in B$$
3		rexnal	$$⊢\exists x\in A\neg y\in B\leftrightarrow \neg \forall x\in Ay\in B$$
4	2 3	sylib	$$⊢\exists x\in AB=\varnothing \to \neg \forall x\in Ay\in B$$
5		eliin	$$⊢y\in \mathrm{V}\to \left(y\in \bigcap _{x\in A}B\leftrightarrow \forall x\in Ay\in B\right)$$
6	5	elv	$$⊢y\in \bigcap _{x\in A}B\leftrightarrow \forall x\in Ay\in B$$
7	4 6	sylnibr	$$⊢\exists x\in AB=\varnothing \to \neg y\in \bigcap _{x\in A}B$$
8	7	eq0rdv	$$⊢\exists x\in AB=\varnothing \to \bigcap _{x\in A}B=\varnothing$$