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

Theorem cbviun 5035
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 2372. See cbviung 5037 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 2891 . . . 4 𝑦 𝑧𝐵
3 cbviun.2 . . . . 5 𝑥𝐶
43nfcri 2891 . . . 4 𝑥 𝑧𝐶
5 cbviun.3 . . . . 5 (𝑥 = 𝑦𝐵 = 𝐶)
65eleq2d 2820 . . . 4 (𝑥 = 𝑦 → (𝑧𝐵𝑧𝐶))
72, 4, 6cbvrexw 3305 . . 3 (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑦𝐴 𝑧𝐶)
87abbii 2803 . 2 {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} = {𝑧 ∣ ∃𝑦𝐴 𝑧𝐶}
9 df-iun 4995 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
10 df-iun 4995 . 2 𝑦𝐴 𝐶 = {𝑧 ∣ ∃𝑦𝐴 𝑧𝐶}
118, 9, 103eqtr4i 2771 1 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  {cab 2710  wnfc 2884  wrex 3071   ciun 4993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-iun 4995
This theorem is referenced by:  cbviunv  5039  disjxiun  5141  funiunfvf  7235  mpomptsx  8037  dmmpossx  8039  fmpox  8040  ovmptss  8066  iunfi  9328  fsum2dlem  15703  fsumcom2  15707  fsumiun  15754  fprod2dlem  15911  fprodcom2  15915  gsumcom2  19826  fiuncmp  22877  ovolfiniun  24987  ovoliunlem3  24990  ovoliun  24991  finiunmbl  25030  volfiniun  25033  iunmbl  25039  limciun  25380  iuneqfzuzlem  43917  fsumiunss  44164  sge0iunmpt  45007  meaiunincf  45072  meaiuninc3  45074  smfliminf  45420  dmmpossx2  46852
  Copyright terms: Public domain W3C validator