# Metamath Proof Explorer

## Theorem cbviun

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) Add disjoint variable condition to avoid ax-13 . See cbviung for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

Ref Expression
Hypotheses cbviun.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
cbviun.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
cbviun.3 ${⊢}{x}={y}\to {B}={C}$
Assertion cbviun ${⊢}\bigcup _{{x}\in {A}}{B}=\bigcup _{{y}\in {A}}{C}$

### Proof

Step Hyp Ref Expression
1 cbviun.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
2 cbviun.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
3 cbviun.3 ${⊢}{x}={y}\to {B}={C}$
4 1 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in {B}$
5 2 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {C}$
6 3 eleq2d ${⊢}{x}={y}\to \left({z}\in {B}↔{z}\in {C}\right)$
7 4 5 6 cbvrexw ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {B}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {C}$
8 7 abbii ${⊢}\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {B}\right\}=\left\{{z}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {C}\right\}$
9 df-iun ${⊢}\bigcup _{{x}\in {A}}{B}=\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {B}\right\}$
10 df-iun ${⊢}\bigcup _{{y}\in {A}}{C}=\left\{{z}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {C}\right\}$
11 8 9 10 3eqtr4i ${⊢}\bigcup _{{x}\in {A}}{B}=\bigcup _{{y}\in {A}}{C}$