Theorem iuneq2dv 4980

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 3125	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		iuneq2 4975	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 17	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∪ ciun 4955

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3449  df-ss 3931  df-iun 4957

This theorem is referenced by:  iuneq12dOLD  4984  iuneq12d  4985  iuneq2d  4986  fparlem3  8093  fparlem4  8094  oalim  8496  omlim  8497  oelim  8498  oelim2  8559  r1val3  9791  imasdsval  17478  acsfn  17620  tgidm  22867  cmpsub  23287  alexsublem  23931  bcth3  25231  ovoliunlem1  25403  voliunlem1  25451  uniiccdif  25479  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem4  25487  itg2monolem1  25651  taylpfval  26272  dmdju  32571  ofpreima2  32590  fnpreimac  32595  ssdifidllem  33427  esum2dlem  34082  eulerpartlemgu  34368  cvmscld  35260  satom  35343  msubvrs  35547  mblfinlem2  37652  ftc1anclem6  37692  heibor  37815  prjspval2  42601  trclfvcom  43712  scottrankd  44237  meaiininclem  46484  carageniuncllem2  46520  hoidmv1le  46592  hoidmvle  46598  ovnhoilem2  46600  ovnhoi  46601  ovnlecvr2  46608  ovncvr2  46609  hspmbl  46627  ovolval4lem1  46647  ovnovollem1  46654  ovnovollem2  46655  iunhoiioo  46674  vonioolem2  46679  smflimlem4  46772  smflimlem6  46774