Theorem cbviunv 5044

Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.) Add disjoint variable condition to avoid ax-13 2372. See cbviunvg 5046 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)

Hypothesis

Ref	Expression
cbviunv.1	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbviunv	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbviunv

Step	Hyp	Ref	Expression
1		nfcv 2904	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2904	. 2 ⊢ Ⅎ𝑥𝐶
3		cbviunv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbviun 5040	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1542  ∪ ciun 4998

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 5000

This theorem is referenced by:  iunxdif2  5057  otiunsndisj  5521  onfununi  8341  oelim2  8595  marypha2lem2  9431  ttrclselem1  9720  ttrclselem2  9721  trcl  9723  r1om  10239  fictb  10240  cfsmolem  10265  cfsmo  10266  domtriomlem  10437  domtriom  10438  pwfseq  10659  wunex2  10733  wuncval2  10742  fsuppmapnn0fiubex  13957  s3iunsndisj  14915  ackbijnn  15774  smndex1basss  18786  smndex1mgm  18788  efgs1b  19604  ablfaclem3  19957  ptbasfi  23085  bcth3  24848  itg1climres  25232  suppovss  31937  hashunif  32049  bnj601  33962  cvmliftlem15  34320  neibastop2  35294  filnetlem4  35314  sstotbnd2  36690  heiborlem3  36729  heibor  36737  lcfr  40504  mapdrval  40566  corclrcl  42506  trclrelexplem  42510  dftrcl3  42519  cotrcltrcl  42524  dfrtrcl3  42532  corcltrcl  42538  cotrclrcl  42541  ssmapsn  43963  cnrefiisplem  44593  cnrefiisp  44594  meaiuninclem  45244  meaiuninc  45245  meaiininc  45251  carageniuncllem2  45286  caratheodorylem1  45290  caratheodorylem2  45291  caratheodory  45292  ovnsubadd  45336  hoidmv1le  45358  hoidmvle  45364  ovnhoilem2  45366  hspmbl  45393  ovnovollem3  45422  vonvolmbl  45425  smflimlem2  45536  smflimlem3  45537  smflimlem4  45538  smflim  45541  smflim2  45570  smflimsup  45592  otiunsndisjX  46035