Theorem iuneq2d 4977

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-v 3442  df-ss 3918  df-iun 4948

This theorem is referenced by:  iununi  5054  oelim2  8523  ituniiun  10332  rtrclreclem1  14980  dfrtrclrec2  14981  rtrclreclem2  14982  rtrclreclem4  14984  imasval  17432  mreacs  17581  pzriprnglem10  21445  cnextval  24005  taylfval  26322  iunpreima  32639  constrlim  33896  reprdifc  34784  msubvrs  35754  neibastop2  36555  voliunnfl  37861  sstotbnd2  37971  equivtotbnd  37975  totbndbnd  37986  heiborlem3  38010  eliunov2  43916  fvmptiunrelexplb0d  43921  fvmptiunrelexplb1d  43923  comptiunov2i  43943  trclrelexplem  43948  dftrcl3  43957  trclfvcom  43960  cnvtrclfv  43961  cotrcltrcl  43962  trclimalb2  43963  trclfvdecomr  43965  dfrtrcl3  43970  dfrtrcl4  43975  isomenndlem  46770  ovnval  46781  hoicvr  46788  hoicvrrex  46796  ovnlecvr  46798  ovncvrrp  46804  ovnsubaddlem1  46810  hoidmvlelem3  46837  hoidmvle  46840  ovnhoilem1  46841  ovnovollem1  46896  smflimlem3  47013  otiunsndisjX  47521