Theorem iuneq2d 5027

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-v 3480  df-ss 3980  df-iun 4998

This theorem is referenced by:  iununi  5104  oelim2  8632  ituniiun  10460  rtrclreclem1  15093  dfrtrclrec2  15094  rtrclreclem2  15095  rtrclreclem4  15097  imasval  17558  mreacs  17703  pzriprnglem10  21519  cnextval  24085  taylfval  26415  iunpreima  32585  constrlim  33744  reprdifc  34621  msubvrs  35545  neibastop2  36344  voliunnfl  37651  sstotbnd2  37761  equivtotbnd  37765  totbndbnd  37776  heiborlem3  37800  eliunov2  43669  fvmptiunrelexplb0d  43674  fvmptiunrelexplb1d  43676  comptiunov2i  43696  trclrelexplem  43701  dftrcl3  43710  trclfvcom  43713  cnvtrclfv  43714  cotrcltrcl  43715  trclimalb2  43716  trclfvdecomr  43718  dfrtrcl3  43723  dfrtrcl4  43728  isomenndlem  46486  ovnval  46497  hoicvr  46504  hoicvrrex  46512  ovnlecvr  46514  ovncvrrp  46520  ovnsubaddlem1  46526  hoidmvlelem3  46553  hoidmvle  46556  ovnhoilem1  46557  ovnovollem1  46612  smflimlem3  46729  otiunsndisjX  47229