Theorem iuneq2dv 4976

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

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

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 3446  df-ss 3928  df-iun 4953

This theorem is referenced by:  iuneq12dOLD  4980  iuneq12d  4981  iuneq2d  4982  fparlem3  8070  fparlem4  8071  oalim  8473  omlim  8474  oelim  8475  oelim2  8536  r1val3  9767  imasdsval  17454  acsfn  17596  tgidm  22843  cmpsub  23263  alexsublem  23907  bcth3  25207  ovoliunlem1  25379  voliunlem1  25427  uniiccdif  25455  uniioombllem2  25460  uniioombllem3a  25461  uniioombllem4  25463  itg2monolem1  25627  taylpfval  26248  dmdju  32544  ofpreima2  32563  fnpreimac  32568  ssdifidllem  33400  esum2dlem  34055  eulerpartlemgu  34341  cvmscld  35233  satom  35316  msubvrs  35520  mblfinlem2  37625  ftc1anclem6  37665  heibor  37788  prjspval2  42574  trclfvcom  43685  scottrankd  44210  meaiininclem  46457  carageniuncllem2  46493  hoidmv1le  46565  hoidmvle  46571  ovnhoilem2  46573  ovnhoi  46574  ovnlecvr2  46581  ovncvr2  46582  hspmbl  46600  ovolval4lem1  46620  ovnovollem1  46627  ovnovollem2  46628  iunhoiioo  46647  vonioolem2  46652  smflimlem4  46745  smflimlem6  46747