Theorem iun0

Description: An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	iun0	⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝑦 ∈ ∅
2	1	a1i	⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝑦 ∈ ∅ )
3	2	nrex	⊢ ¬ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ∅
4		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅ ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ∅ )
5	3 4	mtbir	⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅
6	5	nel0	⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅