Theorem iuneq2d 4950

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ∪ 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:  iununi  5024  oelim2  8388  trpredeq1  9398  trpredeq2  9399  ituniiun  10109  rtrclreclem1  14696  dfrtrclrec2  14697  rtrclreclem2  14698  rtrclreclem4  14700  imasval  17139  mreacs  17284  cnextval  23120  taylfval  25423  iunpreima  30805  reprdifc  32507  msubvrs  33422  neibastop2  34477  voliunnfl  35748  sstotbnd2  35859  equivtotbnd  35863  totbndbnd  35874  heiborlem3  35898  eliunov2  41176  fvmptiunrelexplb0d  41181  fvmptiunrelexplb1d  41183  comptiunov2i  41203  trclrelexplem  41208  dftrcl3  41217  trclfvcom  41220  cnvtrclfv  41221  cotrcltrcl  41222  trclimalb2  41223  trclfvdecomr  41225  dfrtrcl3  41230  dfrtrcl4  41235  isomenndlem  43958  ovnval  43969  hoicvr  43976  hoicvrrex  43984  ovnlecvr  43986  ovncvrrp  43992  ovnsubaddlem1  43998  hoidmvlelem3  44025  hoidmvle  44028  ovnhoilem1  44029  ovnovollem1  44084  smflimlem3  44195  otiunsndisjX  44658