Theorem iuneq2d 4972

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ ciun 4941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3438  df-ss 3920  df-iun 4943

This theorem is referenced by:  iununi  5048  oelim2  8513  ituniiun  10316  rtrclreclem1  14964  dfrtrclrec2  14965  rtrclreclem2  14966  rtrclreclem4  14968  imasval  17415  mreacs  17564  pzriprnglem10  21397  cnextval  23946  taylfval  26264  iunpreima  32508  constrlim  33706  reprdifc  34595  msubvrs  35533  neibastop2  36335  voliunnfl  37644  sstotbnd2  37754  equivtotbnd  37758  totbndbnd  37769  heiborlem3  37793  eliunov2  43652  fvmptiunrelexplb0d  43657  fvmptiunrelexplb1d  43659  comptiunov2i  43679  trclrelexplem  43684  dftrcl3  43693  trclfvcom  43696  cnvtrclfv  43697  cotrcltrcl  43698  trclimalb2  43699  trclfvdecomr  43701  dfrtrcl3  43706  dfrtrcl4  43711  isomenndlem  46511  ovnval  46522  hoicvr  46529  hoicvrrex  46537  ovnlecvr  46539  ovncvrrp  46545  ovnsubaddlem1  46551  hoidmvlelem3  46578  hoidmvle  46581  ovnhoilem1  46582  ovnovollem1  46637  smflimlem3  46754  otiunsndisjX  47263