Theorem iuneq2dv 4966

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

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

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 3438  df-ss 3920  df-iun 4943

This theorem is referenced by:  iuneq12dOLD  4970  iuneq12d  4971  iuneq2d  4972  fparlem3  8047  fparlem4  8048  oalim  8450  omlim  8451  oelim  8452  oelim2  8513  r1val3  9734  imasdsval  17419  acsfn  17565  tgidm  22865  cmpsub  23285  alexsublem  23929  bcth3  25229  ovoliunlem1  25401  voliunlem1  25449  uniiccdif  25477  uniioombllem2  25482  uniioombllem3a  25483  uniioombllem4  25485  itg2monolem1  25649  taylpfval  26270  dmdju  32590  ofpreima2  32609  fnpreimac  32614  ssdifidllem  33393  esum2dlem  34059  eulerpartlemgu  34345  cvmscld  35250  satom  35333  msubvrs  35537  mblfinlem2  37642  ftc1anclem6  37682  heibor  37805  prjspval2  42590  trclfvcom  43700  scottrankd  44225  meaiininclem  46471  carageniuncllem2  46507  hoidmv1le  46579  hoidmvle  46585  ovnhoilem2  46587  ovnhoi  46588  ovnlecvr2  46595  ovncvr2  46596  hspmbl  46614  ovolval4lem1  46634  ovnovollem1  46641  ovnovollem2  46642  iunhoiioo  46661  vonioolem2  46666  smflimlem4  46759  smflimlem6  46761