Theorem iuneq2d 4964

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 4958	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ ciun 4933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-v 3431  df-ss 3906  df-iun 4935

This theorem is referenced by:  iununi  5041  oelim2  8531  ituniiun  10344  rtrclreclem1  15019  dfrtrclrec2  15020  rtrclreclem2  15021  rtrclreclem4  15023  imasval  17475  mreacs  17624  pzriprnglem10  21470  cnextval  24026  taylfval  26324  iunpreima  32634  constrlim  33883  reprdifc  34771  msubvrs  35742  neibastop2  36543  voliunnfl  37985  sstotbnd2  38095  equivtotbnd  38099  totbndbnd  38110  heiborlem3  38134  eliunov2  44106  fvmptiunrelexplb0d  44111  fvmptiunrelexplb1d  44113  comptiunov2i  44133  trclrelexplem  44138  dftrcl3  44147  trclfvcom  44150  cnvtrclfv  44151  cotrcltrcl  44152  trclimalb2  44153  trclfvdecomr  44155  dfrtrcl3  44160  dfrtrcl4  44165  isomenndlem  46958  ovnval  46969  hoicvr  46976  hoicvrrex  46984  ovnlecvr  46986  ovncvrrp  46992  ovnsubaddlem1  46998  hoidmvlelem3  47025  hoidmvle  47028  ovnhoilem1  47029  ovnovollem1  47084  smflimlem3  47201  otiunsndisjX  47727