Theorem iuneq2dv 5021

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-v 3480  df-ss 3980  df-iun 4998

This theorem is referenced by:  iuneq12dOLD  5025  iuneq12d  5026  iuneq2d  5027  fparlem3  8138  fparlem4  8139  oalim  8569  omlim  8570  oelim  8571  oelim2  8632  r1val3  9876  imasdsval  17562  acsfn  17704  tgidm  23003  cmpsub  23424  alexsublem  24068  bcth3  25379  ovoliunlem1  25551  voliunlem1  25599  uniiccdif  25627  uniioombllem2  25632  uniioombllem3a  25633  uniioombllem4  25635  itg2monolem1  25800  taylpfval  26421  dmdju  32664  ofpreima2  32683  fnpreimac  32688  ssdifidllem  33464  esum2dlem  34073  eulerpartlemgu  34359  cvmscld  35258  satom  35341  msubvrs  35545  mblfinlem2  37645  ftc1anclem6  37685  heibor  37808  prjspval2  42600  trclfvcom  43713  scottrankd  44244  meaiininclem  46442  carageniuncllem2  46478  hoidmv1le  46550  hoidmvle  46556  ovnhoilem2  46558  ovnhoi  46559  ovnlecvr2  46566  ovncvr2  46567  hspmbl  46585  ovolval4lem1  46605  ovnovollem1  46612  ovnovollem2  46613  iunhoiioo  46632  vonioolem2  46637  smflimlem4  46730  smflimlem6  46732