Theorem iuneq0

Description: An indexed union is empty iff all indexed classes are empty. (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Assertion	iuneq0	$$⊢\forall x\in AB=\varnothing \leftrightarrow \bigcup _{x\in A}B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		iunss	$$⊢\bigcup _{x\in A}B\subseteq \varnothing \leftrightarrow \forall x\in AB\subseteq \varnothing$$
2		ss0b	$$⊢\bigcup _{x\in A}B\subseteq \varnothing \leftrightarrow \bigcup _{x\in A}B=\varnothing$$
3		ss0b	$$⊢B\subseteq \varnothing \leftrightarrow B=\varnothing$$
4	3	ralbii	$$⊢\forall x\in AB\subseteq \varnothing \leftrightarrow \forall x\in AB=\varnothing$$
5	1 2 4	3bitr3ri	$$⊢\forall x\in AB=\varnothing \leftrightarrow \bigcup _{x\in A}B=\varnothing$$