Theorem iuneq2d 4982

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ ciun 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3446  df-ss 3928  df-iun 4953

This theorem is referenced by:  iununi  5058  oelim2  8536  ituniiun  10351  rtrclreclem1  14999  dfrtrclrec2  15000  rtrclreclem2  15001  rtrclreclem4  15003  imasval  17450  mreacs  17595  pzriprnglem10  21376  cnextval  23924  taylfval  26242  iunpreima  32466  constrlim  33702  reprdifc  34591  msubvrs  35520  neibastop2  36322  voliunnfl  37631  sstotbnd2  37741  equivtotbnd  37745  totbndbnd  37756  heiborlem3  37780  eliunov2  43641  fvmptiunrelexplb0d  43646  fvmptiunrelexplb1d  43648  comptiunov2i  43668  trclrelexplem  43673  dftrcl3  43682  trclfvcom  43685  cnvtrclfv  43686  cotrcltrcl  43687  trclimalb2  43688  trclfvdecomr  43690  dfrtrcl3  43695  dfrtrcl4  43700  isomenndlem  46501  ovnval  46512  hoicvr  46519  hoicvrrex  46527  ovnlecvr  46529  ovncvrrp  46535  ovnsubaddlem1  46541  hoidmvlelem3  46568  hoidmvle  46571  ovnhoilem1  46572  ovnovollem1  46627  smflimlem3  46744  otiunsndisjX  47253