Theorem cbviun 4973

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 2370. See cbviung 4975 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.

Step	Hyp	Ref	Expression
1		cbviun.1	. . . . 5 ⊢ Ⅎ𝑦𝐵
2	1	nfcri 2892	. . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
3		cbviun.2	. . . . 5 ⊢ Ⅎ𝑥𝐶
4	3	nfcri 2892	. . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐶
5		cbviun.3	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
6	5	eleq2d 2822	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
7	2, 4, 6	cbvrexw 3386	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
8	7	abbii 2806	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
9		df-iun 4933	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
10		df-iun 4933	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
11	8, 9, 10	3eqtr4i 2774	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  {cab 2713  Ⅎwnfc 2885  ∃wrex 3071  ∪ ciun 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-11 2152  ax-12 2169  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-iun 4933

This theorem is referenced by:  cbviunv  4977  disjxiun  5078  funiunfvf  7154  mpomptsx  7936  dmmpossx  7938  fmpox  7939  ovmptss  7965  iunfi  9151  fsum2dlem  15527  fsumcom2  15531  fsumiun  15578  fprod2dlem  15735  fprodcom2  15739  gsumcom2  19621  fiuncmp  22600  ovolfiniun  24710  ovoliunlem3  24713  ovoliun  24714  finiunmbl  24753  volfiniun  24756  iunmbl  24762  limciun  25103  iuneqfzuzlem  42921  fsumiunss  43165  sge0iunmpt  44006  meaiunincf  44071  meaiuninc3  44073  smfliminf  44418  dmmpossx2  45730