Theorem iuneq2d 4986

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 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	iuneq2dv 4980	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3449  df-ss 3931  df-iun 4957

This theorem is referenced by:  iununi  5063  oelim2  8559  ituniiun  10375  rtrclreclem1  15023  dfrtrclrec2  15024  rtrclreclem2  15025  rtrclreclem4  15027  imasval  17474  mreacs  17619  pzriprnglem10  21400  cnextval  23948  taylfval  26266  iunpreima  32493  constrlim  33729  reprdifc  34618  msubvrs  35547  neibastop2  36349  voliunnfl  37658  sstotbnd2  37768  equivtotbnd  37772  totbndbnd  37783  heiborlem3  37807  eliunov2  43668  fvmptiunrelexplb0d  43673  fvmptiunrelexplb1d  43675  comptiunov2i  43695  trclrelexplem  43700  dftrcl3  43709  trclfvcom  43712  cnvtrclfv  43713  cotrcltrcl  43714  trclimalb2  43715  trclfvdecomr  43717  dfrtrcl3  43722  dfrtrcl4  43727  isomenndlem  46528  ovnval  46539  hoicvr  46546  hoicvrrex  46554  ovnlecvr  46556  ovncvrrp  46562  ovnsubaddlem1  46568  hoidmvlelem3  46595  hoidmvle  46598  ovnhoilem1  46599  ovnovollem1  46654  smflimlem3  46771  otiunsndisjX  47280