Theorem iuneq2dv 4969

Description: Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)

Hypothesis

Ref	Expression
iuneq2dv.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
iuneq2dv	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem iuneq2dv

Step	Hyp	Ref	Expression
1		iuneq2dv.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
2	1	ralrimiva 3126	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		iuneq2 4964	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 17	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3049  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-v 3440  df-ss 3916  df-iun 4946

This theorem is referenced by:  iuneq12dOLD  4973  iuneq12d  4974  iuneq2d  4975  fparlem3  8054  fparlem4  8055  oalim  8457  omlim  8458  oelim  8459  oelim2  8521  r1val3  9748  imasdsval  17434  acsfn  17580  tgidm  22922  cmpsub  23342  alexsublem  23986  bcth3  25285  ovoliunlem1  25457  voliunlem1  25505  uniiccdif  25533  uniioombllem2  25538  uniioombllem3a  25539  uniioombllem4  25541  itg2monolem1  25705  taylpfval  26326  dmdju  32674  ofpreima2  32693  fnpreimac  32698  ssdifidllem  33486  esum2dlem  34198  eulerpartlemgu  34483  cvmscld  35416  satom  35499  msubvrs  35703  mblfinlem2  37798  ftc1anclem6  37838  heibor  37961  prjspval2  42798  trclfvcom  43906  scottrankd  44431  meaiininclem  46672  carageniuncllem2  46708  hoidmv1le  46780  hoidmvle  46786  ovnhoilem2  46788  ovnhoi  46789  ovnlecvr2  46796  ovncvr2  46797  hspmbl  46815  ovolval4lem1  46835  ovnovollem1  46842  ovnovollem2  46843  iunhoiioo  46862  vonioolem2  46867  smflimlem4  46960  smflimlem6  46962