MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbviun Unicode version

Theorem cbviun 4070
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.
StepHypRef Expression
1 cbviun.1 . . . . 5  |-  F/_ y B
21nfcri 2518 . . . 4  |-  F/ y  z  e.  B
3 cbviun.2 . . . . 5  |-  F/_ x C
43nfcri 2518 . . . 4  |-  F/ x  z  e.  C
5 cbviun.3 . . . . 5  |-  ( x  =  y  ->  B  =  C )
65eleq2d 2455 . . . 4  |-  ( x  =  y  ->  (
z  e.  B  <->  z  e.  C ) )
72, 4, 6cbvrex 2873 . . 3  |-  ( E. x  e.  A  z  e.  B  <->  E. y  e.  A  z  e.  C )
87abbii 2500 . 2  |-  { z  |  E. x  e.  A  z  e.  B }  =  { z  |  E. y  e.  A  z  e.  C }
9 df-iun 4038 . 2  |-  U_ x  e.  A  B  =  { z  |  E. x  e.  A  z  e.  B }
10 df-iun 4038 . 2  |-  U_ y  e.  A  C  =  { z  |  E. y  e.  A  z  e.  C }
118, 9, 103eqtr4i 2418 1  |-  U_ x  e.  A  B  =  U_ y  e.  A  C
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   {cab 2374   F/_wnfc 2511   E.wrex 2651   U_ciun 4036
This theorem is referenced by:  cbviunv  4072  disjxiun  4151  funiunfvf  5936  mpt2mptsx  6354  dmmpt2ssx  6356  fmpt2x  6357  ovmptss  6368  iunfi  7331  fsum2dlem  12482  fsumcom2  12486  fsumiun  12528  gsumcom2  15477  fiuncmp  17390  ovolfiniun  19265  ovoliunlem3  19268  ovoliun  19269  finiunmbl  19306  volfiniun  19309  iunmbl  19315  limciun  19649
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ral 2655  df-rex 2656  df-iun 4038
  Copyright terms: Public domain W3C validator