Theorem iuneq2d 4987

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3457  df-ss 3922  df-iun 4958

This theorem is referenced by:  iununi  5065  oelim2  8577  ituniiun  10401  rtrclreclem1  15090  dfrtrclrec2  15091  rtrclreclem2  15092  rtrclreclem4  15094  imasval  17560  mreacs  17709  pzriprnglem10  21640  cnextval  24218  taylfval  26522  iunpreima  32909  constrlim  34129  reprdifc  35014  msubvrs  36052  nmulprop  36682  neibastop2  36872  voliunnfl  38315  sstotbnd2  38425  equivtotbnd  38429  totbndbnd  38440  heiborlem3  38464  eliunov2  44405  fvmptiunrelexplb0d  44410  fvmptiunrelexplb1d  44412  comptiunov2i  44432  trclrelexplem  44437  dftrcl3  44446  trclfvcom  44449  cnvtrclfv  44450  cotrcltrcl  44451  trclimalb2  44452  trclfvdecomr  44454  dfrtrcl3  44459  dfrtrcl4  44464  isomenndlem  47244  ovnval  47255  hoicvr  47262  hoicvrrex  47270  ovnlecvr  47272  ovncvrrp  47278  ovnsubaddlem1  47284  hoidmvlelem3  47311  hoidmvle  47314  ovnhoilem1  47315  ovnovollem1  47370  smflimlem3  47487  otiunsndisjX  48016