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

Metamath Proof Explorer

Theorem iuneq12df

Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016)

Ref Expression
Hypotheses iuneq12df.1 ⊢ Ⅎ x φ
iuneq12df.2 ⊢ Ⅎ _ x A
iuneq12df.3 ⊢ Ⅎ _ x B
iuneq12df.4 ⊢ φ → A = B
iuneq12df.5 ⊢ φ → C = D
Assertion iuneq12df ⊢ φ → ⋃ x ∈ A C = ⋃ x ∈ B D

Proof

Step Hyp Ref Expression
1 iuneq12df.1 ⊢ Ⅎ x φ
2 iuneq12df.2 ⊢ Ⅎ _ x A
3 iuneq12df.3 ⊢ Ⅎ _ x B
4 iuneq12df.4 ⊢ φ → A = B
5 iuneq12df.5 ⊢ φ → C = D
6 5 eleq2d ⊢ φ → y ∈ C ↔ y ∈ D
7 1 2 3 4 6 rexeqbid ⊢ φ → ∃ x ∈ A y ∈ C ↔ ∃ x ∈ B y ∈ D
8 7 alrimiv ⊢ φ → ∀ y ∃ x ∈ A y ∈ C ↔ ∃ x ∈ B y ∈ D
9 abbi ⊢ ∀ y ∃ x ∈ A y ∈ C ↔ ∃ x ∈ B y ∈ D → y | ∃ x ∈ A y ∈ C = y | ∃ x ∈ B y ∈ D
10 df-iun ⊢ ⋃ x ∈ A C = y | ∃ x ∈ A y ∈ C
11 df-iun ⊢ ⋃ x ∈ B D = y | ∃ x ∈ B y ∈ D
12 9 10 11 3eqtr4g ⊢ ∀ y ∃ x ∈ A y ∈ C ↔ ∃ x ∈ B y ∈ D → ⋃ x ∈ A C = ⋃ x ∈ B D
13 8 12 syl ⊢ φ → ⋃ x ∈ A C = ⋃ x ∈ B D