Theorem iuneq2dv 4945

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-in 3890  df-ss 3900  df-iun 4923

This theorem is referenced by:  iuneq12d  4949  iuneq2d  4950  fparlem3  7925  fparlem4  7926  oalim  8324  omlim  8325  oelim  8326  oelim2  8388  r1val3  9527  imasdsval  17143  acsfn  17285  tgidm  22038  cmpsub  22459  alexsublem  23103  bcth3  24400  ovoliunlem1  24571  voliunlem1  24619  uniiccdif  24647  uniioombllem2  24652  uniioombllem3a  24653  uniioombllem4  24655  itg2monolem1  24820  taylpfval  25429  ofpreima2  30905  fnpreimac  30910  esum2dlem  31960  eulerpartlemgu  32244  cvmscld  33135  satom  33218  msubvrs  33422  mblfinlem2  35742  ftc1anclem6  35782  heibor  35906  prjspval2  40373  trclfvcom  41220  scottrankd  41755  meaiininclem  43914  carageniuncllem2  43950  hoidmv1le  44022  hoidmvle  44028  ovnhoilem2  44030  ovnhoi  44031  ovnlecvr2  44038  ovncvr2  44039  hspmbl  44057  ovolval4lem1  44077  ovnovollem1  44084  ovnovollem2  44085  iunhoiioo  44104  vonioolem2  44109  smflimlem4  44196  smflimlem6  44198