Theorem iuneq2d 4979

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3444  df-ss 3920  df-iun 4950

This theorem is referenced by:  iununi  5056  oelim2  8533  ituniiun  10344  rtrclreclem1  14992  dfrtrclrec2  14993  rtrclreclem2  14994  rtrclreclem4  14996  imasval  17444  mreacs  17593  pzriprnglem10  21457  cnextval  24017  taylfval  26334  iunpreima  32651  constrlim  33917  reprdifc  34805  msubvrs  35776  neibastop2  36577  voliunnfl  37915  sstotbnd2  38025  equivtotbnd  38029  totbndbnd  38040  heiborlem3  38064  eliunov2  44035  fvmptiunrelexplb0d  44040  fvmptiunrelexplb1d  44042  comptiunov2i  44062  trclrelexplem  44067  dftrcl3  44076  trclfvcom  44079  cnvtrclfv  44080  cotrcltrcl  44081  trclimalb2  44082  trclfvdecomr  44084  dfrtrcl3  44089  dfrtrcl4  44094  isomenndlem  46888  ovnval  46899  hoicvr  46906  hoicvrrex  46914  ovnlecvr  46916  ovncvrrp  46922  ovnsubaddlem1  46928  hoidmvlelem3  46955  hoidmvle  46958  ovnhoilem1  46959  ovnovollem1  47014  smflimlem3  47131  otiunsndisjX  47639