Theorem iuneq2dv 4978

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∀wral 3079  ∪ ciun 4953

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3455  df-ss 3900  df-iun 4955

This theorem is used by:  iuneq12d  4982  iuneq2d  4983  fparlem3  8135  fparlem4  8136  oalim  8551  omlim  8552  oelim  8553  oelim2  8615  r1val3  9860  scottrankd  9959  imasdsval  17699  acsfn  17845  ssdifidllem  21652  tgidm  23310  cmpsub  23730  alexsublem  24375  bcth3  25664  ovoliunlem1  25835  voliunlem1  25883  uniiccdif  25911  uniioombllem2  25916  uniioombllem3a  25917  uniioombllem4  25919  itg2monolem1  26083  taylpfval  26704  dmdju  33295  ofpreima2  33314  fnpreimac  33318  esum2dlem  34777  eulerpartlemgu  35062  cvmscld  36159  satom  36242  msubvrs  36446  mblfinlem2  38716  ftc1anclem6  38756  heibor  38895  prjspval2  43781  trclfvcom  44863  meaiininclem  47635  carageniuncllem2  47671  hoidmv1le  47743  hoidmvle  47749  ovnhoilem2  47751  ovnhoi  47752  ovnlecvr2  47759  ovncvr2  47760  hspmbl  47778  ovolval4lem1  47798  ovnovollem1  47805  ovnovollem2  47806  iunhoiioo  47825  vonioolem2  47830  smflimlem4  47923  smflimlem6  47925