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  37865  sstotbnd2  37975  equivtotbnd  37979  totbndbnd  37990  heiborlem3  38014  eliunov2  43920  fvmptiunrelexplb0d  43925  fvmptiunrelexplb1d  43927  comptiunov2i  43947  trclrelexplem  43952  dftrcl3  43961  trclfvcom  43964  cnvtrclfv  43965  cotrcltrcl  43966  trclimalb2  43967  trclfvdecomr  43969  dfrtrcl3  43974  dfrtrcl4  43979  isomenndlem  46774  ovnval  46785  hoicvr  46792  hoicvrrex  46800  ovnlecvr  46802  ovncvrrp  46808  ovnsubaddlem1  46814  hoidmvlelem3  46841  hoidmvle  46844  ovnhoilem1  46845  ovnovollem1  46900  smflimlem3  47017  otiunsndisjX  47525