Theorem iuneq2dv 4985

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-v 3465  df-ss 3930  df-iun 4962

This theorem is referenced by:  iuneq12dOLD  4989  iuneq12d  4990  iuneq2d  4991  fparlem3  8109  fparlem4  8110  oalim  8517  omlim  8518  oelim  8519  oelim2  8581  r1val3  9810  scottrankd  9874  imasdsval  17569  acsfn  17715  ssdifidllem  21453  tgidm  23106  cmpsub  23526  alexsublem  24170  bcth3  25459  ovoliunlem1  25630  voliunlem1  25678  uniiccdif  25706  uniioombllem2  25711  uniioombllem3a  25712  uniioombllem4  25714  itg2monolem1  25878  taylpfval  26494  dmdju  32933  ofpreima2  32952  fnpreimac  32956  esum2dlem  34427  eulerpartlemgu  34712  cvmscld  35664  satom  35747  msubvrs  35951  mblfinlem2  38197  ftc1anclem6  38237  heibor  38360  prjspval2  43237  trclfvcom  44341  meaiininclem  47092  carageniuncllem2  47128  hoidmv1le  47200  hoidmvle  47206  ovnhoilem2  47208  ovnhoi  47209  ovnlecvr2  47216  ovncvr2  47217  hspmbl  47235  ovolval4lem1  47255  ovnovollem1  47262  ovnovollem2  47263  iunhoiioo  47282  vonioolem2  47287  smflimlem4  47380  smflimlem6  47382