Theorem iuneq2d 4953

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  ∪ ciun 4924

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-in 3894  df-ss 3904  df-iun 4926

This theorem is referenced by:  iununi  5028  oelim2  8426  ituniiun  10178  rtrclreclem1  14768  dfrtrclrec2  14769  rtrclreclem2  14770  rtrclreclem4  14772  imasval  17222  mreacs  17367  cnextval  23212  taylfval  25518  iunpreima  30904  reprdifc  32607  msubvrs  33522  neibastop2  34550  voliunnfl  35821  sstotbnd2  35932  equivtotbnd  35936  totbndbnd  35947  heiborlem3  35971  eliunov2  41287  fvmptiunrelexplb0d  41292  fvmptiunrelexplb1d  41294  comptiunov2i  41314  trclrelexplem  41319  dftrcl3  41328  trclfvcom  41331  cnvtrclfv  41332  cotrcltrcl  41333  trclimalb2  41334  trclfvdecomr  41336  dfrtrcl3  41341  dfrtrcl4  41346  isomenndlem  44068  ovnval  44079  hoicvr  44086  hoicvrrex  44094  ovnlecvr  44096  ovncvrrp  44102  ovnsubaddlem1  44108  hoidmvlelem3  44135  hoidmvle  44138  ovnhoilem1  44139  ovnovollem1  44194  smflimlem3  44308  otiunsndisjX  44771