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

Theorem cbviun 5041
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 2375. See cbviung 5043 for a less restrictive version requiring more axioms. (Revised by GG, 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 2895 . . . 4 𝑦 𝑧𝐵
3 cbviun.2 . . . . 5 𝑥𝐶
43nfcri 2895 . . . 4 𝑥 𝑧𝐶
5 cbviun.3 . . . . 5 (𝑥 = 𝑦𝐵 = 𝐶)
65eleq2d 2825 . . . 4 (𝑥 = 𝑦 → (𝑧𝐵𝑧𝐶))
72, 4, 6cbvrexw 3305 . . 3 (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑦𝐴 𝑧𝐶)
87abbii 2807 . 2 {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} = {𝑧 ∣ ∃𝑦𝐴 𝑧𝐶}
9 df-iun 4998 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
10 df-iun 4998 . 2 𝑦𝐴 𝐶 = {𝑧 ∣ ∃𝑦𝐴 𝑧𝐶}
118, 9, 103eqtr4i 2773 1 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2106  {cab 2712  wnfc 2888  wrex 3068   ciun 4996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-iun 4998
This theorem is referenced by:  disjxiun  5145  funiunfvf  7269  mpomptsx  8088  dmmpossx  8090  fmpox  8091  ovmptss  8117  iunfi  9381  fsum2dlem  15803  fsumcom2  15807  fsumiun  15854  fprod2dlem  16013  fprodcom2  16017  gsumcom2  20008  fiuncmp  23428  ovolfiniun  25550  ovoliunlem3  25553  ovoliun  25554  finiunmbl  25593  volfiniun  25596  iunmbl  25602  limciun  25944  iuneqfzuzlem  45284  fsumiunss  45531  sge0iunmpt  46374  meaiunincf  46439  meaiuninc3  46441  smfliminf  46787  dmmpossx2  48182
  Copyright terms: Public domain W3C validator