Theorem iuneq2d 4980

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3897  df-iun 4952

This theorem is used by:  iununi  5058  iunpreima  7073  oelim2  8611  ituniiun  10507  rtrclreclem1  15219  dfrtrclrec2  15220  rtrclreclem2  15221  rtrclreclem4  15223  imasval  17692  mreacs  17841  pzriprnglem10  21805  cnextval  24389  taylfval  26695  constrlim  34421  reprdifc  35306  msubvrs  36415  nmulprop  37035  neibastop2  37245  voliunnfl  38691  sstotbnd2  38817  equivtotbnd  38821  totbndbnd  38832  heiborlem3  38856  eliunov2  44788  fvmptiunrelexplb0d  44793  fvmptiunrelexplb1d  44795  comptiunov2i  44815  trclrelexplem  44820  dftrcl3  44829  trclfvcom  44832  cnvtrclfv  44833  cotrcltrcl  44834  trclimalb2  44835  trclfvdecomr  44837  dfrtrcl3  44842  dfrtrcl4  44847  isomenndlem  47648  ovnval  47659  hoicvr  47666  hoicvrrex  47674  ovnlecvr  47676  ovncvrrp  47682  ovnsubaddlem1  47688  hoidmvlelem3  47715  hoidmvle  47718  ovnhoilem1  47719  ovnovollem1  47774  smflimlem3  47891  otiunsndisjX  48457