Theorem iuneq2d 4986

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ∪ ciun 4956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-ss 3901  df-iun 4958

This theorem is used by:  iununi  5064  iunpreima  7100  oelim2  8642  ituniiun  10539  rtrclreclem1  15253  dfrtrclrec2  15254  rtrclreclem2  15255  rtrclreclem4  15257  imasval  17733  mreacs  17882  pzriprnglem10  21851  cnextval  24435  taylfval  26743  constrlim  34482  reprdifc  35367  msubvrs  36533  nmulprop  37154  neibastop2  37364  voliunnfl  38850  sstotbnd2  38974  equivtotbnd  38978  totbndbnd  38989  heiborlem3  39013  eliunov2  44940  fvmptiunrelexplb0d  44945  fvmptiunrelexplb1d  44947  comptiunov2i  44967  trclrelexplem  44972  dftrcl3  44981  trclfvcom  44984  cnvtrclfv  44985  cotrcltrcl  44986  trclimalb2  44987  trclfvdecomr  44989  dfrtrcl3  44994  dfrtrcl4  44999  isomenndlem  47813  ovnval  47824  hoicvr  47831  hoicvrrex  47839  ovnlecvr  47841  ovncvrrp  47847  ovnsubaddlem1  47853  hoidmvlelem3  47880  hoidmvle  47883  ovnhoilem1  47884  ovnovollem1  47939  smflimlem3  48056  otiunsndisjX  48622