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

Theorem cbviun 4367
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
cbviun.2
cbviun.3
Assertion
Ref Expression
cbviun
Distinct variable groups:   ,   ,

Proof of Theorem cbviun
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cbviun.1 . . . . 5
21nfcri 2612 . . . 4
3 cbviun.2 . . . . 5
43nfcri 2612 . . . 4
5 cbviun.3 . . . . 5
65eleq2d 2527 . . . 4
72, 4, 6cbvrex 3081 . . 3
87abbii 2591 . 2
9 df-iun 4332 . 2
10 df-iun 4332 . 2
118, 9, 103eqtr4i 2496 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  {cab 2442  F/_wnfc 2605  E.wrex 2808  U_ciun 4330
This theorem is referenced by:  cbviunv  4369  disjxiun  4449  funiunfvf  6161  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  ovmptss  6881  iunfi  7828  fsum2dlem  13585  fsumcom2  13589  fsumiun  13635  fprod2dlem  13784  fprodcom2  13788  gsumcom2  17003  fiuncmp  19904  ovolfiniun  21912  ovoliunlem3  21915  ovoliun  21916  finiunmbl  21954  volfiniun  21957  iunmbl  21963  limciun  22298  dmmpt2ssx2  32926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-iun 4332
  Copyright terms: Public domain W3C validator