Theorem iuneq2dv 4974

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∀wral 3076  ∪ ciun 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-v 3456  df-ss 3921  df-iun 4951

This theorem is referenced by:  iuneq12dOLD  4978  iuneq12d  4979  iuneq2d  4980  fparlem3  8093  fparlem4  8094  oalim  8501  omlim  8502  oelim  8503  oelim2  8565  r1val3  9796  imasdsval  17545  acsfn  17691  tgidm  23040  cmpsub  23460  alexsublem  24104  bcth3  25393  ovoliunlem1  25564  voliunlem1  25612  uniiccdif  25640  uniioombllem2  25645  uniioombllem3a  25646  uniioombllem4  25648  itg2monolem1  25812  taylpfval  26428  dmdju  32849  ofpreima2  32868  fnpreimac  32872  ssdifidllem  33643  esum2dlem  34389  eulerpartlemgu  34674  cvmscld  35623  satom  35706  msubvrs  35910  mblfinlem2  38157  ftc1anclem6  38197  heibor  38320  prjspval2  43195  trclfvcom  44299  scottrankd  44824  meaiininclem  47060  carageniuncllem2  47096  hoidmv1le  47168  hoidmvle  47174  ovnhoilem2  47176  ovnhoi  47177  ovnlecvr2  47184  ovncvr2  47185  hspmbl  47203  ovolval4lem1  47223  ovnovollem1  47230  ovnovollem2  47231  iunhoiioo  47250  vonioolem2  47255  smflimlem4  47348  smflimlem6  47350