Theorem iuneq2d 5025

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-v 3476  df-in 3954  df-ss 3964  df-iun 4998

This theorem is referenced by:  iununi  5101  oelim2  8591  ituniiun  10413  rtrclreclem1  15000  dfrtrclrec2  15001  rtrclreclem2  15002  rtrclreclem4  15004  imasval  17453  mreacs  17598  cnextval  23556  taylfval  25862  iunpreima  31783  reprdifc  33627  msubvrs  34539  neibastop2  35234  voliunnfl  36520  sstotbnd2  36630  equivtotbnd  36634  totbndbnd  36645  heiborlem3  36669  eliunov2  42415  fvmptiunrelexplb0d  42420  fvmptiunrelexplb1d  42422  comptiunov2i  42442  trclrelexplem  42447  dftrcl3  42456  trclfvcom  42459  cnvtrclfv  42460  cotrcltrcl  42461  trclimalb2  42462  trclfvdecomr  42464  dfrtrcl3  42469  dfrtrcl4  42474  isomenndlem  45232  ovnval  45243  hoicvr  45250  hoicvrrex  45258  ovnlecvr  45260  ovncvrrp  45266  ovnsubaddlem1  45272  hoidmvlelem3  45299  hoidmvle  45302  ovnhoilem1  45303  ovnovollem1  45358  smflimlem3  45475  otiunsndisjX  45973