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

Theorem cbviun 4952
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.) Add disjoint variable condition to avoid ax-13 2381. See cbviung 4954 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
Hypotheses
Ref Expression
cbviun.1 𝑦𝐵
cbviun.2 𝑥𝐶
cbviun.3 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbviun 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Distinct variable group:   𝑥,𝑦,𝐴
Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem cbviun
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cbviun.1 . . . . 5 𝑦𝐵
21nfcri 2968 . . . 4 𝑦 𝑧𝐵
3 cbviun.2 . . . . 5 𝑥𝐶
43nfcri 2968 . . . 4 𝑥 𝑧𝐶
5 cbviun.3 . . . . 5 (𝑥 = 𝑦𝐵 = 𝐶)
65eleq2d 2895 . . . 4 (𝑥 = 𝑦 → (𝑧𝐵𝑧𝐶))
72, 4, 6cbvrexw 3440 . . 3 (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑦𝐴 𝑧𝐶)
87abbii 2883 . 2 {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} = {𝑧 ∣ ∃𝑦𝐴 𝑧𝐶}
9 df-iun 4912 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
10 df-iun 4912 . 2 𝑦𝐴 𝐶 = {𝑧 ∣ ∃𝑦𝐴 𝑧𝐶}
118, 9, 103eqtr4i 2851 1 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  {cab 2796  wnfc 2958  wrex 3136   ciun 4910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-iun 4912
This theorem is referenced by:  cbviunv  4956  disjxiun  5054  funiunfvf  6999  mpomptsx  7751  dmmpossx  7753  fmpox  7754  ovmptss  7777  iunfi  8800  fsum2dlem  15113  fsumcom2  15117  fsumiun  15164  fprod2dlem  15322  fprodcom2  15326  gsumcom2  19024  fiuncmp  21940  ovolfiniun  24029  ovoliunlem3  24032  ovoliun  24033  finiunmbl  24072  volfiniun  24075  iunmbl  24081  limciun  24419  iuneqfzuzlem  41478  fsumiunss  41732  sge0iunmpt  42577  meaiunincf  42642  meaiuninc3  42644  smfliminf  42982  dmmpossx2  44313
  Copyright terms: Public domain W3C validator