Theorem iuneq2dv 4942

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138  ∪ ciun 4918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-in 3942  df-ss 3951  df-iun 4920

This theorem is referenced by:  iuneq12d  4946  iuneq2d  4947  fparlem3  7808  fparlem4  7809  oalim  8156  omlim  8157  oelim  8158  oelim2  8220  r1val3  9266  imasdsval  16787  acsfn  16929  tgidm  21587  cmpsub  22007  alexsublem  22651  bcth3  23933  ovoliunlem1  24102  voliunlem1  24150  uniiccdif  24178  uniioombllem2  24183  uniioombllem3a  24184  uniioombllem4  24186  itg2monolem1  24350  taylpfval  24952  ofpreima2  30410  fnpreimac  30415  esum2dlem  31351  eulerpartlemgu  31635  cvmscld  32520  satom  32603  msubvrs  32807  mblfinlem2  34929  ftc1anclem6  34971  heibor  35098  prjspval2  39261  trclfvcom  40066  scottrankd  40582  meaiininclem  42767  carageniuncllem2  42803  hoidmv1le  42875  hoidmvle  42881  ovnhoilem2  42883  ovnhoi  42884  ovnlecvr2  42891  ovncvr2  42892  hspmbl  42910  ovolval4lem1  42930  ovnovollem1  42937  ovnovollem2  42938  iunhoiioo  42957  vonioolem2  42962  smflimlem4  43049  smflimlem6  43051