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 ⊢ ⋃ x ∈ A ⋃ y ∈ B C = z | ∃ x ∈ A ∃ y ∈ B z ∈ C

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ⋃ y ∈ B C = w | ∃ y ∈ B w ∈ C
2 1 a1i ⊢ x ∈ A → ⋃ y ∈ B C = w | ∃ y ∈ B w ∈ C
3 2 iuneq2i ⊢ ⋃ x ∈ A ⋃ y ∈ B C = ⋃ x ∈ A w | ∃ y ∈ B w ∈ C
4 df-iun ⊢ ⋃ x ∈ A w | ∃ y ∈ B w ∈ C = z | ∃ x ∈ A z ∈ w | ∃ y ∈ B w ∈ C
5 vex ⊢ z ∈ V
6 eleq1w ⊢ w = z → w ∈ C ↔ z ∈ C
7 6 rexbidv ⊢ w = z → ∃ y ∈ B w ∈ C ↔ ∃ y ∈ B z ∈ C
8 5 7 elab ⊢ z ∈ w | ∃ y ∈ B w ∈ C ↔ ∃ y ∈ B z ∈ C
9 8 rexbii ⊢ ∃ x ∈ A z ∈ w | ∃ y ∈ B w ∈ C ↔ ∃ x ∈ A ∃ y ∈ B z ∈ C
10 9 abbii ⊢ z | ∃ x ∈ A z ∈ w | ∃ y ∈ B w ∈ C = z | ∃ x ∈ A ∃ y ∈ B z ∈ C
11 3 4 10 3eqtri ⊢ ⋃ x ∈ A ⋃ y ∈ B C = z | ∃ x ∈ A ∃ y ∈ B z ∈ C