Theorem iuneq2d 4998

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∪ ciun 4967

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-v 3461  df-ss 3943  df-iun 4969

This theorem is referenced by:  iununi  5075  oelim2  8607  ituniiun  10436  rtrclreclem1  15076  dfrtrclrec2  15077  rtrclreclem2  15078  rtrclreclem4  15080  imasval  17525  mreacs  17670  pzriprnglem10  21451  cnextval  23999  taylfval  26318  iunpreima  32545  constrlim  33773  reprdifc  34659  msubvrs  35582  neibastop2  36379  voliunnfl  37688  sstotbnd2  37798  equivtotbnd  37802  totbndbnd  37813  heiborlem3  37837  eliunov2  43703  fvmptiunrelexplb0d  43708  fvmptiunrelexplb1d  43710  comptiunov2i  43730  trclrelexplem  43735  dftrcl3  43744  trclfvcom  43747  cnvtrclfv  43748  cotrcltrcl  43749  trclimalb2  43750  trclfvdecomr  43752  dfrtrcl3  43757  dfrtrcl4  43762  isomenndlem  46559  ovnval  46570  hoicvr  46577  hoicvrrex  46585  ovnlecvr  46587  ovncvrrp  46593  ovnsubaddlem1  46599  hoidmvlelem3  46626  hoidmvle  46629  ovnhoilem1  46630  ovnovollem1  46685  smflimlem3  46802  otiunsndisjX  47308