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

Theorem cbviun 4589
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:   𝑦,𝐴   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem cbviun
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cbviun.1 . . . . 5 𝑦𝐵
21nfcri 2787 . . . 4 𝑦 𝑧𝐵
3 cbviun.2 . . . . 5 𝑥𝐶
43nfcri 2787 . . . 4 𝑥 𝑧𝐶
5 cbviun.3 . . . . 5 (𝑥 = 𝑦𝐵 = 𝐶)
65eleq2d 2716 . . . 4 (𝑥 = 𝑦 → (𝑧𝐵𝑧𝐶))
72, 4, 6cbvrex 3198 . . 3 (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑦𝐴 𝑧𝐶)
87abbii 2768 . 2 {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} = {𝑧 ∣ ∃𝑦𝐴 𝑧𝐶}
9 df-iun 4554 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
10 df-iun 4554 . 2 𝑦𝐴 𝐶 = {𝑧 ∣ ∃𝑦𝐴 𝑧𝐶}
118, 9, 103eqtr4i 2683 1 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  {cab 2637  wnfc 2780  wrex 2942   ciun 4552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-iun 4554
This theorem is referenced by:  cbviunv  4591  disjxiun  4681  disjxiunOLD  4682  funiunfvf  6547  mpt2mptsx  7278  dmmpt2ssx  7280  fmpt2x  7281  ovmptss  7303  iunfi  8295  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fsumiun  14597  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  gsumcom2  18420  fiuncmp  21255  ovolfiniun  23315  ovoliunlem3  23318  ovoliun  23319  finiunmbl  23358  volfiniun  23361  iunmbl  23367  limciun  23703  iuneqfzuzlem  39863  fsumiunss  40125  sge0iunmpt  40953  meaiunincf  41018  meaiuninc3  41020  smfliminf  41358  dmmpt2ssx2  42440
  Copyright terms: Public domain W3C validator