Theorem iuneq2dv 4964

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∪ ciun 4939

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-v 3438  df-ss 3914  df-iun 4941

This theorem is referenced by:  iuneq12dOLD  4968  iuneq12d  4969  iuneq2d  4970  fparlem3  8044  fparlem4  8045  oalim  8447  omlim  8448  oelim  8449  oelim2  8510  r1val3  9731  imasdsval  17419  acsfn  17565  tgidm  22895  cmpsub  23315  alexsublem  23959  bcth3  25258  ovoliunlem1  25430  voliunlem1  25478  uniiccdif  25506  uniioombllem2  25511  uniioombllem3a  25512  uniioombllem4  25514  itg2monolem1  25678  taylpfval  26299  dmdju  32629  ofpreima2  32648  fnpreimac  32653  ssdifidllem  33421  esum2dlem  34105  eulerpartlemgu  34390  cvmscld  35317  satom  35400  msubvrs  35604  mblfinlem2  37708  ftc1anclem6  37748  heibor  37871  prjspval2  42716  trclfvcom  43826  scottrankd  44351  meaiininclem  46594  carageniuncllem2  46630  hoidmv1le  46702  hoidmvle  46708  ovnhoilem2  46710  ovnhoi  46711  ovnlecvr2  46718  ovncvr2  46719  hspmbl  46737  ovolval4lem1  46757  ovnovollem1  46764  ovnovollem2  46765  iunhoiioo  46784  vonioolem2  46789  smflimlem4  46882  smflimlem6  46884