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	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = ∅ ↔ ∪ 𝑥 ∈ 𝐴 𝐵 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∅ ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∅ )
2		ss0b	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∅ ↔ ∪ 𝑥 ∈ 𝐴 𝐵 = ∅ )
3		ss0b	⊢ ( 𝐵 ⊆ ∅ ↔ 𝐵 = ∅ )
4	3	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∅ ↔ ∀ 𝑥 ∈ 𝐴 𝐵 = ∅ )
5	1 2 4	3bitr3ri	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = ∅ ↔ ∪ 𝑥 ∈ 𝐴 𝐵 = ∅ )