Theorem iuneq2dv 5016

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∪ ciun 4991

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-iun 4993

This theorem is referenced by:  iuneq12dOLD  5020  iuneq12d  5021  iuneq2d  5022  fparlem3  8139  fparlem4  8140  oalim  8570  omlim  8571  oelim  8572  oelim2  8633  r1val3  9878  imasdsval  17560  acsfn  17702  tgidm  22987  cmpsub  23408  alexsublem  24052  bcth3  25365  ovoliunlem1  25537  voliunlem1  25585  uniiccdif  25613  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem4  25621  itg2monolem1  25785  taylpfval  26406  dmdju  32657  ofpreima2  32676  fnpreimac  32681  ssdifidllem  33484  esum2dlem  34093  eulerpartlemgu  34379  cvmscld  35278  satom  35361  msubvrs  35565  mblfinlem2  37665  ftc1anclem6  37705  heibor  37828  prjspval2  42623  trclfvcom  43736  scottrankd  44267  meaiininclem  46501  carageniuncllem2  46537  hoidmv1le  46609  hoidmvle  46615  ovnhoilem2  46617  ovnhoi  46618  ovnlecvr2  46625  ovncvr2  46626  hspmbl  46644  ovolval4lem1  46664  ovnovollem1  46671  ovnovollem2  46672  iunhoiioo  46691  vonioolem2  46696  smflimlem4  46789  smflimlem6  46791