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

Metamath Proof Explorer

Theorem iuneq12daf

Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017)

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

Proof

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