Theorem iuneq2dv 4948

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∪ ciun 4924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-in 3894  df-ss 3904  df-iun 4926

This theorem is referenced by:  iuneq12d  4952  iuneq2d  4953  fparlem3  7954  fparlem4  7955  oalim  8362  omlim  8363  oelim  8364  oelim2  8426  r1val3  9596  imasdsval  17226  acsfn  17368  tgidm  22130  cmpsub  22551  alexsublem  23195  bcth3  24495  ovoliunlem1  24666  voliunlem1  24714  uniiccdif  24742  uniioombllem2  24747  uniioombllem3a  24748  uniioombllem4  24750  itg2monolem1  24915  taylpfval  25524  ofpreima2  31003  fnpreimac  31008  esum2dlem  32060  eulerpartlemgu  32344  cvmscld  33235  satom  33318  msubvrs  33522  mblfinlem2  35815  ftc1anclem6  35855  heibor  35979  prjspval2  40452  trclfvcom  41331  scottrankd  41866  meaiininclem  44024  carageniuncllem2  44060  hoidmv1le  44132  hoidmvle  44138  ovnhoilem2  44140  ovnhoi  44141  ovnlecvr2  44148  ovncvr2  44149  hspmbl  44167  ovolval4lem1  44187  ovnovollem1  44194  ovnovollem2  44195  iunhoiioo  44214  vonioolem2  44219  smflimlem4  44309  smflimlem6  44311