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

Metamath Proof Explorer

Theorem dfiunv2

Description: Define double indexed union. (Contributed by FL, 6-Nov-2013)

Ref Expression
Assertion dfiunv2 ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 }

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ∪ 𝑦 ∈ 𝐵 𝐶 = { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 }
2 1 a1i ⊢ ( 𝑥 ∈ 𝐴 → ∪ 𝑦 ∈ 𝐵 𝐶 = { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } )
3 2 iuneq2i ⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐴 { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 }
4 df-iun ⊢ ∪ 𝑥 ∈ 𝐴 { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } }
5 vex ⊢ 𝑧 ∈ V
6 eleq1w ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶 ) )
7 6 rexbidv ⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 ) )
8 5 7 elab ⊢ ( 𝑧 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
9 8 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
10 9 abbii ⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐵 𝑤 ∈ 𝐶 } } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 }
11 3 4 10 3eqtri ⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 }