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
`|- F/_ y B`
cbviun.2
`|- F/_ x C`
cbviun.3
`|- ( x = y -> B = C )`
Assertion cbviun
`|- U_ x e. A B = U_ y e. A C`

Proof

Step Hyp Ref Expression
1 cbviun.1
` |-  F/_ y B`
2 cbviun.2
` |-  F/_ x C`
3 cbviun.3
` |-  ( x = y -> B = C )`
4 1 nfcri
` |-  F/ y z e. B`
5 2 nfcri
` |-  F/ x z e. C`
6 3 eleq2d
` |-  ( x = y -> ( z e. B <-> z e. C ) )`
7 4 5 6 cbvrexw
` |-  ( E. x e. A z e. B <-> E. y e. A z e. C )`
8 7 abbii
` |-  { z | E. x e. A z e. B } = { z | E. y e. A z e. C }`
9 df-iun
` |-  U_ x e. A B = { z | E. x e. A z e. B }`
10 df-iun
` |-  U_ y e. A C = { z | E. y e. A z e. C }`
11 8 9 10 3eqtr4i
` |-  U_ x e. A B = U_ y e. A C`