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

Metamath Proof Explorer

Theorem cbviunf

Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006) (Revised by Andrew Salmon, 25-Jul-2011)

Ref Expression
Hypotheses cbviunf.x ⊢ Ⅎ _ x A
cbviunf.y ⊢ Ⅎ _ y A
cbviunf.1 ⊢ Ⅎ _ y B
cbviunf.2 ⊢ Ⅎ _ x C
cbviunf.3 ⊢ x = y → B = C
Assertion cbviunf ⊢ ⋃ x ∈ A B = ⋃ y ∈ A C

Proof

Step Hyp Ref Expression
1 cbviunf.x ⊢ Ⅎ _ x A
2 cbviunf.y ⊢ Ⅎ _ y A
3 cbviunf.1 ⊢ Ⅎ _ y B
4 cbviunf.2 ⊢ Ⅎ _ x C
5 cbviunf.3 ⊢ x = y → B = C
6 3 nfcri ⊢ Ⅎ y z ∈ B
7 4 nfcri ⊢ Ⅎ x z ∈ C
8 5 eleq2d ⊢ x = y → z ∈ B ↔ z ∈ C
9 1 2 6 7 8 cbvrexfw ⊢ ∃ x ∈ A z ∈ B ↔ ∃ y ∈ A z ∈ C
10 9 abbii ⊢ z | ∃ x ∈ A z ∈ B = z | ∃ y ∈ A z ∈ C
11 df-iun ⊢ ⋃ x ∈ A B = z | ∃ x ∈ A z ∈ B
12 df-iun ⊢ ⋃ y ∈ A C = z | ∃ y ∈ A z ∈ C
13 10 11 12 3eqtr4i ⊢ ⋃ x ∈ A B = ⋃ y ∈ A C