Theorem iuneq2d 5027

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-in 3956  df-ss 3966  df-iun 5000

This theorem is referenced by:  iununi  5103  oelim2  8595  ituniiun  10417  rtrclreclem1  15004  dfrtrclrec2  15005  rtrclreclem2  15006  rtrclreclem4  15008  imasval  17457  mreacs  17602  cnextval  23565  taylfval  25871  iunpreima  31827  reprdifc  33670  msubvrs  34582  neibastop2  35294  voliunnfl  36580  sstotbnd2  36690  equivtotbnd  36694  totbndbnd  36705  heiborlem3  36729  eliunov2  42478  fvmptiunrelexplb0d  42483  fvmptiunrelexplb1d  42485  comptiunov2i  42505  trclrelexplem  42510  dftrcl3  42519  trclfvcom  42522  cnvtrclfv  42523  cotrcltrcl  42524  trclimalb2  42525  trclfvdecomr  42527  dfrtrcl3  42532  dfrtrcl4  42537  isomenndlem  45294  ovnval  45305  hoicvr  45312  hoicvrrex  45320  ovnlecvr  45322  ovncvrrp  45328  ovnsubaddlem1  45334  hoidmvlelem3  45361  hoidmvle  45364  ovnhoilem1  45365  ovnovollem1  45420  smflimlem3  45537  otiunsndisjX  46035  pzriprnglem10  46862