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  31906  hashunif  32018  bnj601  33931  cvmliftlem15  34289  neibastop2  35246  filnetlem4  35266  sstotbnd2  36642  heiborlem3  36681  heibor  36689  lcfr  40456  mapdrval  40518  corclrcl  42458  trclrelexplem  42462  dftrcl3  42471  cotrcltrcl  42476  dfrtrcl3  42484  corcltrcl  42490  cotrclrcl  42493  ssmapsn  43915  cnrefiisplem  44545  cnrefiisp  44546  meaiuninclem  45196  meaiuninc  45197  meaiininc  45203  carageniuncllem2  45238  caratheodorylem1  45242  caratheodorylem2  45243  caratheodory  45244  ovnsubadd  45288  hoidmv1le  45310  hoidmvle  45316  ovnhoilem2  45318  hspmbl  45345  ovnovollem3  45374  vonvolmbl  45377  smflimlem2  45488  smflimlem3  45489  smflimlem4  45490  smflim  45493  smflim2  45522  smflimsup  45544  otiunsndisjX  45987