Theorem iuneq2d 4967

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ∪ ciun 4936

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-v 3438  df-ss 3914  df-iun 4938

This theorem is referenced by:  iununi  5042  oelim2  8505  ituniiun  10308  rtrclreclem1  14959  dfrtrclrec2  14960  rtrclreclem2  14961  rtrclreclem4  14963  imasval  17410  mreacs  17559  pzriprnglem10  21422  cnextval  23971  taylfval  26288  iunpreima  32536  constrlim  33744  reprdifc  34632  msubvrs  35596  neibastop2  36395  voliunnfl  37704  sstotbnd2  37814  equivtotbnd  37818  totbndbnd  37829  heiborlem3  37853  eliunov2  43712  fvmptiunrelexplb0d  43717  fvmptiunrelexplb1d  43719  comptiunov2i  43739  trclrelexplem  43744  dftrcl3  43753  trclfvcom  43756  cnvtrclfv  43757  cotrcltrcl  43758  trclimalb2  43759  trclfvdecomr  43761  dfrtrcl3  43766  dfrtrcl4  43771  isomenndlem  46568  ovnval  46579  hoicvr  46586  hoicvrrex  46594  ovnlecvr  46596  ovncvrrp  46602  ovnsubaddlem1  46608  hoidmvlelem3  46635  hoidmvle  46638  ovnhoilem1  46639  ovnovollem1  46694  smflimlem3  46811  otiunsndisjX  47310