Theorem iuneq2d 5045

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-ss 3993  df-iun 5017

This theorem is referenced by:  iununi  5122  oelim2  8651  ituniiun  10491  rtrclreclem1  15106  dfrtrclrec2  15107  rtrclreclem2  15108  rtrclreclem4  15110  imasval  17571  mreacs  17716  pzriprnglem10  21524  cnextval  24090  taylfval  26418  iunpreima  32587  constrlim  33729  reprdifc  34604  msubvrs  35528  neibastop2  36327  voliunnfl  37624  sstotbnd2  37734  equivtotbnd  37738  totbndbnd  37749  heiborlem3  37773  eliunov2  43641  fvmptiunrelexplb0d  43646  fvmptiunrelexplb1d  43648  comptiunov2i  43668  trclrelexplem  43673  dftrcl3  43682  trclfvcom  43685  cnvtrclfv  43686  cotrcltrcl  43687  trclimalb2  43688  trclfvdecomr  43690  dfrtrcl3  43695  dfrtrcl4  43700  isomenndlem  46451  ovnval  46462  hoicvr  46469  hoicvrrex  46477  ovnlecvr  46479  ovncvrrp  46485  ovnsubaddlem1  46491  hoidmvlelem3  46518  hoidmvle  46521  ovnhoilem1  46522  ovnovollem1  46577  smflimlem3  46694  otiunsndisjX  47194