Theorem cbviun 4328

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.)

Hypotheses

Ref	Expression
cbviun.1	|- F/_ y B
cbviun.2	|- F/_ x C
cbviun.3	|- ( x = y -> B = C )

Assertion

Ref	Expression
cbviun	|- U_ x e. A B = U_ y e. A C

Distinct variable groups:   y, A   x, A

Allowed substitution hints:   B( x, y)   C( x, y)

Proof of Theorem cbviun

Dummy variable z is distinct from all other variables.

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

Syntax hints:   -> wi 4   = wceq 1454   e. wcel 1897   {cab 2447   F/_wnfc 2589   E.wrex 2749   U_ciun 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-iun 4293

This theorem is referenced by:  cbviunv  4330  disjxiun  4412  funiunfvf  6178  mpt2mptsx  6882  dmmpt2ssx  6884  fmpt2x  6885  ovmptss  6903  iunfi  7887  fsum2dlem  13879  fsumcom2  13883  fsumiun  13929  fprod2dlem  14082  fprodcom2  14086  gsumcom2  17655  fiuncmp  20467  ovolfiniun  22502  ovoliunlem3  22505  ovoliun  22506  finiunmbl  22545  volfiniun  22548  iunmbl  22554  limciun  22897  iuneqfzuzlem  37594  fsumiunss  37691  sge0iunmpt  38297  dmmpt2ssx2  40390