Theorem iuneq2dv 4983

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  ∪ ciun 4958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-ss 3923  df-iun 4960

This theorem is used by:  iuneq12dOLD  4987  iuneq12d  4988  iuneq2d  4989  fparlem3  8115  fparlem4  8116  oalim  8523  omlim  8524  oelim  8525  oelim2  8587  r1val3  9817  scottrankd  9885  imasdsval  17593  acsfn  17739  ssdifidllem  21536  tgidm  23189  cmpsub  23609  alexsublem  24254  bcth3  25543  ovoliunlem1  25714  voliunlem1  25762  uniiccdif  25790  uniioombllem2  25795  uniioombllem3a  25796  uniioombllem4  25798  itg2monolem1  25962  taylpfval  26581  dmdju  33065  ofpreima2  33084  fnpreimac  33088  esum2dlem  34548  eulerpartlemgu  34834  cvmscld  35804  satom  35887  msubvrs  36091  mblfinlem2  38368  ftc1anclem6  38408  heibor  38532  prjspval2  43405  trclfvcom  44509  meaiininclem  47260  carageniuncllem2  47296  hoidmv1le  47368  hoidmvle  47374  ovnhoilem2  47376  ovnhoi  47377  ovnlecvr2  47384  ovncvr2  47385  hspmbl  47403  ovolval4lem1  47423  ovnovollem1  47430  ovnovollem2  47431  iunhoiioo  47450  vonioolem2  47455  smflimlem4  47548  smflimlem6  47550