Theorem iuneq2d 4955

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ∪ ciun 4926

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 2109  ax-9 2117  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3067  df-rex 3068  df-v 3429  df-in 3895  df-ss 3905  df-iun 4928

This theorem is referenced by:  iununi  5029  oelim2  8393  trpredeq1  9414  trpredeq2  9415  ituniiun  10125  rtrclreclem1  14712  dfrtrclrec2  14713  rtrclreclem2  14714  rtrclreclem4  14716  imasval  17166  mreacs  17311  cnextval  23156  taylfval  25461  iunpreima  30845  reprdifc  32549  msubvrs  33464  neibastop2  34519  voliunnfl  35790  sstotbnd2  35901  equivtotbnd  35905  totbndbnd  35916  heiborlem3  35940  eliunov2  41218  fvmptiunrelexplb0d  41223  fvmptiunrelexplb1d  41225  comptiunov2i  41245  trclrelexplem  41250  dftrcl3  41259  trclfvcom  41262  cnvtrclfv  41263  cotrcltrcl  41264  trclimalb2  41265  trclfvdecomr  41267  dfrtrcl3  41272  dfrtrcl4  41277  isomenndlem  44000  ovnval  44011  hoicvr  44018  hoicvrrex  44026  ovnlecvr  44028  ovncvrrp  44034  ovnsubaddlem1  44040  hoidmvlelem3  44067  hoidmvle  44070  ovnhoilem1  44071  ovnovollem1  44126  smflimlem3  44237  otiunsndisjX  44700