Theorem iuneq2d 4989

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-ss 3923  df-iun 4960

This theorem is used by:  iununi  5067  oelim2  8587  ituniiun  10421  rtrclreclem1  15118  dfrtrclrec2  15119  rtrclreclem2  15120  rtrclreclem4  15122  imasval  17587  mreacs  17736  pzriprnglem10  21690  cnextval  24269  taylfval  26573  iunpreima  32980  constrlim  34193  reprdifc  35079  msubvrs  36089  nmulprop  36719  neibastop2  36929  voliunnfl  38372  sstotbnd2  38483  equivtotbnd  38487  totbndbnd  38498  heiborlem3  38522  eliunov2  44463  fvmptiunrelexplb0d  44468  fvmptiunrelexplb1d  44470  comptiunov2i  44490  trclrelexplem  44495  dftrcl3  44504  trclfvcom  44507  cnvtrclfv  44508  cotrcltrcl  44509  trclimalb2  44510  trclfvdecomr  44512  dfrtrcl3  44517  dfrtrcl4  44522  isomenndlem  47302  ovnval  47313  hoicvr  47320  hoicvrrex  47328  ovnlecvr  47330  ovncvrrp  47336  ovnsubaddlem1  47342  hoidmvlelem3  47369  hoidmvle  47372  ovnhoilem1  47373  ovnovollem1  47428  smflimlem3  47545  otiunsndisjX  48074