Theorem iuneq2dv 4958

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∪ ciun 4933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-v 3431  df-ss 3906  df-iun 4935

This theorem is referenced by:  iuneq12dOLD  4962  iuneq12d  4963  iuneq2d  4964  fparlem3  8064  fparlem4  8065  oalim  8467  omlim  8468  oelim  8469  oelim2  8531  r1val3  9762  imasdsval  17479  acsfn  17625  tgidm  22945  cmpsub  23365  alexsublem  24009  bcth3  25298  ovoliunlem1  25469  voliunlem1  25517  uniiccdif  25545  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem4  25553  itg2monolem1  25717  taylpfval  26330  dmdju  32720  ofpreima2  32739  fnpreimac  32743  ssdifidllem  33516  esum2dlem  34236  eulerpartlemgu  34521  cvmscld  35455  satom  35538  msubvrs  35742  mblfinlem2  37979  ftc1anclem6  38019  heibor  38142  prjspval2  43046  trclfvcom  44150  scottrankd  44675  meaiininclem  46914  carageniuncllem2  46950  hoidmv1le  47022  hoidmvle  47028  ovnhoilem2  47030  ovnhoi  47031  ovnlecvr2  47038  ovncvr2  47039  hspmbl  47057  ovolval4lem1  47077  ovnovollem1  47084  ovnovollem2  47085  iunhoiioo  47104  vonioolem2  47109  smflimlem4  47202  smflimlem6  47204