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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-v 3452  df-ss 3934  df-iun 4960

This theorem is referenced by:  iuneq12dOLD  4987  iuneq12d  4988  iuneq2d  4989  fparlem3  8096  fparlem4  8097  oalim  8499  omlim  8500  oelim  8501  oelim2  8562  r1val3  9798  imasdsval  17485  acsfn  17627  tgidm  22874  cmpsub  23294  alexsublem  23938  bcth3  25238  ovoliunlem1  25410  voliunlem1  25458  uniiccdif  25486  uniioombllem2  25491  uniioombllem3a  25492  uniioombllem4  25494  itg2monolem1  25658  taylpfval  26279  dmdju  32578  ofpreima2  32597  fnpreimac  32602  ssdifidllem  33434  esum2dlem  34089  eulerpartlemgu  34375  cvmscld  35267  satom  35350  msubvrs  35554  mblfinlem2  37659  ftc1anclem6  37699  heibor  37822  prjspval2  42608  trclfvcom  43719  scottrankd  44244  meaiininclem  46491  carageniuncllem2  46527  hoidmv1le  46599  hoidmvle  46605  ovnhoilem2  46607  ovnhoi  46608  ovnlecvr2  46615  ovncvr2  46616  hspmbl  46634  ovolval4lem1  46654  ovnovollem1  46661  ovnovollem2  46662  iunhoiioo  46681  vonioolem2  46686  smflimlem4  46779  smflimlem6  46781