Metamath Proof Explorer

Theorem imaiun

Description: The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion imaiun ⊢ A ⋃ x ∈ B C = ⋃ x ∈ B A C

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢ ∃ x ∈ B ∃ z z ∈ C ∧ z y ∈ A ↔ ∃ z ∃ x ∈ B z ∈ C ∧ z y ∈ A
2 vex ⊢ y ∈ V
3 2 elima3 ⊢ y ∈ A C ↔ ∃ z z ∈ C ∧ z y ∈ A
4 3 rexbii ⊢ ∃ x ∈ B y ∈ A C ↔ ∃ x ∈ B ∃ z z ∈ C ∧ z y ∈ A
5 eliun ⊢ z ∈ ⋃ x ∈ B C ↔ ∃ x ∈ B z ∈ C
6 5 anbi1i ⊢ z ∈ ⋃ x ∈ B C ∧ z y ∈ A ↔ ∃ x ∈ B z ∈ C ∧ z y ∈ A
7 r19.41v ⊢ ∃ x ∈ B z ∈ C ∧ z y ∈ A ↔ ∃ x ∈ B z ∈ C ∧ z y ∈ A
8 6 7 bitr4i ⊢ z ∈ ⋃ x ∈ B C ∧ z y ∈ A ↔ ∃ x ∈ B z ∈ C ∧ z y ∈ A
9 8 exbii ⊢ ∃ z z ∈ ⋃ x ∈ B C ∧ z y ∈ A ↔ ∃ z ∃ x ∈ B z ∈ C ∧ z y ∈ A
10 1 4 9 3bitr4ri ⊢ ∃ z z ∈ ⋃ x ∈ B C ∧ z y ∈ A ↔ ∃ x ∈ B y ∈ A C
11 2 elima3 ⊢ y ∈ A ⋃ x ∈ B C ↔ ∃ z z ∈ ⋃ x ∈ B C ∧ z y ∈ A
12 eliun ⊢ y ∈ ⋃ x ∈ B A C ↔ ∃ x ∈ B y ∈ A C
13 10 11 12 3bitr4i ⊢ y ∈ A ⋃ x ∈ B C ↔ y ∈ ⋃ x ∈ B A C
14 13 eqriv ⊢ A ⋃ x ∈ B C = ⋃ x ∈ B A C