This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0iun

Description: An empty indexed union is empty. (Contributed by NM, 4-Dec-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion 0iun ⊢ ⋃ x ∈ ∅ A = ∅

Proof

Step Hyp Ref Expression
1 rex0 ⊢ ¬ ∃ x ∈ ∅ y ∈ A
2 eliun ⊢ y ∈ ⋃ x ∈ ∅ A ↔ ∃ x ∈ ∅ y ∈ A
3 1 2 mtbir ⊢ ¬ y ∈ ⋃ x ∈ ∅ A
4 3 nel0 ⊢ ⋃ x ∈ ∅ A = ∅