Theorem iuneq2d 4780

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

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  ∪ ciun 4753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-v 3400  df-in 3799  df-ss 3806  df-iun 4755

This theorem is referenced by:  iununi  4844  oelim2  7959  ituniiun  9579  dfrtrclrec2  14204  rtrclreclem1  14205  rtrclreclem2  14206  rtrclreclem4  14208  imasval  16557  mreacs  16704  cnextval  22273  taylfval  24550  iunpreima  29945  reprdifc  31307  msubvrs  32056  trpredeq1  32308  trpredeq2  32309  neibastop2  32944  voliunnfl  34081  sstotbnd2  34199  equivtotbnd  34203  totbndbnd  34214  heiborlem3  34238  eliunov2  38932  fvmptiunrelexplb0d  38937  fvmptiunrelexplb1d  38939  comptiunov2i  38959  trclrelexplem  38964  dftrcl3  38973  trclfvcom  38976  cnvtrclfv  38977  cotrcltrcl  38978  trclimalb2  38979  trclfvdecomr  38981  dfrtrcl3  38986  dfrtrcl4  38991  isomenndlem  41675  ovnval  41686  hoicvr  41693  hoicvrrex  41701  ovnlecvr  41703  ovncvrrp  41709  ovnsubaddlem1  41715  hoidmvlelem3  41742  hoidmvle  41745  ovnhoilem1  41746  ovnovollem1  41801  smflimlem3  41912  otiunsndisjX  42324