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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105  ∀wral 3060  ∪ ciun 4997

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-v 3475  df-in 3955  df-ss 3965  df-iun 4999

This theorem is referenced by:  iuneq12d  5025  iuneq2d  5026  fparlem3  8104  fparlem4  8105  oalim  8536  omlim  8537  oelim  8538  oelim2  8599  r1val3  9837  imasdsval  17466  acsfn  17608  tgidm  22704  cmpsub  23125  alexsublem  23769  bcth3  25080  ovoliunlem1  25252  voliunlem1  25300  uniiccdif  25328  uniioombllem2  25333  uniioombllem3a  25334  uniioombllem4  25336  itg2monolem1  25501  taylpfval  26114  ofpreima2  32159  fnpreimac  32164  esum2dlem  33389  eulerpartlemgu  33675  cvmscld  34563  satom  34646  msubvrs  34850  mblfinlem2  36830  ftc1anclem6  36870  heibor  36993  prjspval2  41658  trclfvcom  42777  scottrankd  43310  meaiininclem  45501  carageniuncllem2  45537  hoidmv1le  45609  hoidmvle  45615  ovnhoilem2  45617  ovnhoi  45618  ovnlecvr2  45625  ovncvr2  45626  hspmbl  45644  ovolval4lem1  45664  ovnovollem1  45671  ovnovollem2  45672  iunhoiioo  45691  vonioolem2  45696  smflimlem4  45789  smflimlem6  45791