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

Metamath Proof Explorer

Theorem cbviung

Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. Usage of this theorem is discouraged because it depends on ax-13 . See cbviun for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 26-Mar-2006) (Revised by Andrew Salmon, 25-Jul-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cbviung.1 
|- F/_ y B
cbviung.2 
|- F/_ x C
cbviung.3 
|- ( x = y -> B = C )
Assertion cbviung 
|- U_ x e. A B = U_ y e. A C

Proof

Step Hyp Ref Expression
1 cbviung.1 
 |-  F/_ y B
2 cbviung.2 
 |-  F/_ x C
3 cbviung.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 cbvrex 
 |-  ( 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