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

Metamath Proof Explorer

Theorem iunxprg

Description: A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018)

Ref Expression
Hypotheses iunxprg.1 ⊢ x = A → C = D
iunxprg.2 ⊢ x = B → C = E
Assertion iunxprg ⊢ A ∈ V ∧ B ∈ W → ⋃ x ∈ A B C = D ∪ E

Proof

Step Hyp Ref Expression
1 iunxprg.1 ⊢ x = A → C = D
2 iunxprg.2 ⊢ x = B → C = E
3 df-pr ⊢ A B = A ∪ B
4 iuneq1 ⊢ A B = A ∪ B → ⋃ x ∈ A B C = ⋃ x ∈ A ∪ B C
5 3 4 ax-mp ⊢ ⋃ x ∈ A B C = ⋃ x ∈ A ∪ B C
6 iunxun ⊢ ⋃ x ∈ A ∪ B C = ⋃ x ∈ A C ∪ ⋃ x ∈ B C
7 5 6 eqtri ⊢ ⋃ x ∈ A B C = ⋃ x ∈ A C ∪ ⋃ x ∈ B C
8 1 iunxsng ⊢ A ∈ V → ⋃ x ∈ A C = D
9 8 adantr ⊢ A ∈ V ∧ B ∈ W → ⋃ x ∈ A C = D
10 2 iunxsng ⊢ B ∈ W → ⋃ x ∈ B C = E
11 10 adantl ⊢ A ∈ V ∧ B ∈ W → ⋃ x ∈ B C = E
12 9 11 uneq12d ⊢ A ∈ V ∧ B ∈ W → ⋃ x ∈ A C ∪ ⋃ x ∈ B C = D ∪ E
13 7 12 eqtrid ⊢ A ∈ V ∧ B ∈ W → ⋃ x ∈ A B C = D ∪ E