Theorem iuneq2d 4952

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-v 3433  df-ss 3900  df-iun 4923

This theorem is referenced by:  iununi  5028  oelim2  8521  ituniiun  10335  rtrclreclem1  15010  dfrtrclrec2  15011  rtrclreclem2  15012  rtrclreclem4  15014  imasval  17466  mreacs  17615  pzriprnglem10  21465  cnextval  24044  taylfval  26342  iunpreima  32653  constrlim  33923  reprdifc  34811  msubvrs  35788  neibastop2  36589  voliunnfl  38031  sstotbnd2  38141  equivtotbnd  38145  totbndbnd  38156  heiborlem3  38180  eliunov2  44123  fvmptiunrelexplb0d  44128  fvmptiunrelexplb1d  44130  comptiunov2i  44150  trclrelexplem  44155  dftrcl3  44164  trclfvcom  44167  cnvtrclfv  44168  cotrcltrcl  44169  trclimalb2  44170  trclfvdecomr  44172  dfrtrcl3  44177  dfrtrcl4  44182  isomenndlem  46973  ovnval  46984  hoicvr  46991  hoicvrrex  46999  ovnlecvr  47001  ovncvrrp  47007  ovnsubaddlem1  47013  hoidmvlelem3  47040  hoidmvle  47043  ovnhoilem1  47044  ovnovollem1  47099  smflimlem3  47216  otiunsndisjX  47742