Theorem iuneq2d 4981

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3916  df-iun 4953

This theorem is used by:  iununi  5059  iunpreima  7061  oelim2  8583  ituniiun  10424  rtrclreclem1  15130  dfrtrclrec2  15131  rtrclreclem2  15132  rtrclreclem4  15134  imasval  17597  mreacs  17746  pzriprnglem10  21703  cnextval  24287  taylfval  26595  constrlim  34249  reprdifc  35135  msubvrs  36139  nmulprop  36770  neibastop2  36980  voliunnfl  38413  sstotbnd2  38524  equivtotbnd  38528  totbndbnd  38539  heiborlem3  38563  eliunov2  44519  fvmptiunrelexplb0d  44524  fvmptiunrelexplb1d  44526  comptiunov2i  44546  trclrelexplem  44551  dftrcl3  44560  trclfvcom  44563  cnvtrclfv  44564  cotrcltrcl  44565  trclimalb2  44566  trclfvdecomr  44568  dfrtrcl3  44573  dfrtrcl4  44578  isomenndlem  47358  ovnval  47369  hoicvr  47376  hoicvrrex  47384  ovnlecvr  47386  ovncvrrp  47392  ovnsubaddlem1  47398  hoidmvlelem3  47425  hoidmvle  47428  ovnhoilem1  47429  ovnovollem1  47484  smflimlem3  47601  otiunsndisjX  48167