Theorem iuneq2d 4980

Description: Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)

Hypothesis

Ref	Expression
iuneq2d.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
iuneq2d	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq2d

Step	Hyp	Ref	Expression
1		iuneq2d.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	adantr 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	iuneq2dv 4974	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ∪ 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:  iununi  5056  oelim2  8565  ituniiun  10379  rtrclreclem1  15070  dfrtrclrec2  15071  rtrclreclem2  15072  rtrclreclem4  15074  imasval  17541  mreacs  17690  pzriprnglem10  21539  cnextval  24118  taylfval  26419  iunpreima  32761  constrlim  34033  reprdifc  34918  msubvrs  35907  nmulprop  36537  neibastop2  36718  voliunnfl  38160  sstotbnd2  38270  equivtotbnd  38274  totbndbnd  38285  heiborlem3  38309  eliunov2  44252  fvmptiunrelexplb0d  44257  fvmptiunrelexplb1d  44259  comptiunov2i  44279  trclrelexplem  44284  dftrcl3  44293  trclfvcom  44296  cnvtrclfv  44297  cotrcltrcl  44298  trclimalb2  44299  trclfvdecomr  44301  dfrtrcl3  44306  dfrtrcl4  44311  isomenndlem  47101  ovnval  47112  hoicvr  47119  hoicvrrex  47127  ovnlecvr  47129  ovncvrrp  47135  ovnsubaddlem1  47141  hoidmvlelem3  47168  hoidmvle  47171  ovnhoilem1  47172  ovnovollem1  47227  smflimlem3  47344  otiunsndisjX  47870