Theorem iuneq2d 4991

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 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	iuneq2dv 4985	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-v 3465  df-ss 3930  df-iun 4962

This theorem is referenced by:  iununi  5069  oelim2  8580  ituniiun  10405  rtrclreclem1  15093  dfrtrclrec2  15094  rtrclreclem2  15095  rtrclreclem4  15097  imasval  17564  mreacs  17713  pzriprnglem10  21608  cnextval  24186  taylfval  26487  iunpreima  32849  constrlim  34073  reprdifc  34958  msubvrs  35950  nmulprop  36580  neibastop2  36760  voliunnfl  38202  sstotbnd2  38312  equivtotbnd  38316  totbndbnd  38327  heiborlem3  38351  eliunov2  44296  fvmptiunrelexplb0d  44301  fvmptiunrelexplb1d  44303  comptiunov2i  44323  trclrelexplem  44328  dftrcl3  44337  trclfvcom  44340  cnvtrclfv  44341  cotrcltrcl  44342  trclimalb2  44343  trclfvdecomr  44345  dfrtrcl3  44350  dfrtrcl4  44355  isomenndlem  47135  ovnval  47146  hoicvr  47153  hoicvrrex  47161  ovnlecvr  47163  ovncvrrp  47169  ovnsubaddlem1  47175  hoidmvlelem3  47202  hoidmvle  47205  ovnhoilem1  47206  ovnovollem1  47261  smflimlem3  47378  otiunsndisjX  47904