Theorem iuneq2d 4910

Description: Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)

Hypothesis

Ref	Expression
iuneq2d.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
iuneq2d	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq2d

Step	Hyp	Ref	Expression
1		iuneq2d.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	adantr 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	iuneq2dv 4905	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ∪ ciun 4881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-in 3888  df-ss 3898  df-iun 4883

This theorem is referenced by:  iununi  4984  oelim2  8204  ituniiun  9833  rtrclreclem1  14408  dfrtrclrec2  14409  rtrclreclem2  14410  rtrclreclem4  14412  imasval  16776  mreacs  16921  cnextval  22666  taylfval  24954  iunpreima  30328  reprdifc  32008  msubvrs  32920  trpredeq1  33172  trpredeq2  33173  neibastop2  33822  voliunnfl  35101  sstotbnd2  35212  equivtotbnd  35216  totbndbnd  35227  heiborlem3  35251  eliunov2  40380  fvmptiunrelexplb0d  40385  fvmptiunrelexplb1d  40387  comptiunov2i  40407  trclrelexplem  40412  dftrcl3  40421  trclfvcom  40424  cnvtrclfv  40425  cotrcltrcl  40426  trclimalb2  40427  trclfvdecomr  40429  dfrtrcl3  40434  dfrtrcl4  40439  isomenndlem  43169  ovnval  43180  hoicvr  43187  hoicvrrex  43195  ovnlecvr  43197  ovncvrrp  43203  ovnsubaddlem1  43209  hoidmvlelem3  43236  hoidmvle  43239  ovnhoilem1  43240  ovnovollem1  43295  smflimlem3  43406  otiunsndisjX  43835