Theorem iuneq2d 4974

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∪ ciun 4943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-v 3439  df-ss 3915  df-iun 4945

This theorem is referenced by:  iununi  5051  oelim2  8519  ituniiun  10324  rtrclreclem1  14971  dfrtrclrec2  14972  rtrclreclem2  14973  rtrclreclem4  14975  imasval  17423  mreacs  17572  pzriprnglem10  21436  cnextval  23996  taylfval  26313  iunpreima  32565  constrlim  33824  reprdifc  34712  msubvrs  35676  neibastop2  36477  voliunnfl  37777  sstotbnd2  37887  equivtotbnd  37891  totbndbnd  37902  heiborlem3  37926  eliunov2  43836  fvmptiunrelexplb0d  43841  fvmptiunrelexplb1d  43843  comptiunov2i  43863  trclrelexplem  43868  dftrcl3  43877  trclfvcom  43880  cnvtrclfv  43881  cotrcltrcl  43882  trclimalb2  43883  trclfvdecomr  43885  dfrtrcl3  43890  dfrtrcl4  43895  isomenndlem  46690  ovnval  46701  hoicvr  46708  hoicvrrex  46716  ovnlecvr  46718  ovncvrrp  46724  ovnsubaddlem1  46730  hoidmvlelem3  46757  hoidmvle  46760  ovnhoilem1  46761  ovnovollem1  46816  smflimlem3  46933  otiunsndisjX  47441