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	|- ( A. x e. A B = (/) <-> U_ x e. A B = (/) )

Proof

Step	Hyp	Ref	Expression
1		iunss	|- ( U_ x e. A B C_ (/) <-> A. x e. A B C_ (/) )
2		ss0b	|- ( U_ x e. A B C_ (/) <-> U_ x e. A B = (/) )
3		ss0b	|- ( B C_ (/) <-> B = (/) )
4	3	ralbii	|- ( A. x e. A B C_ (/) <-> A. x e. A B = (/) )
5	1 2 4	3bitr3ri	|- ( A. x e. A B = (/) <-> U_ x e. A B = (/) )