Theorem iuneq2d 5020

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  ∪ ciun 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-rex 3066  df-v 3471  df-in 3951  df-ss 3961  df-iun 4993

This theorem is referenced by:  iununi  5096  oelim2  8609  ituniiun  10439  rtrclreclem1  15030  dfrtrclrec2  15031  rtrclreclem2  15032  rtrclreclem4  15034  imasval  17486  mreacs  17631  pzriprnglem10  21409  cnextval  23958  taylfval  26286  iunpreima  32348  reprdifc  34249  msubvrs  35160  neibastop2  35835  voliunnfl  37126  sstotbnd2  37236  equivtotbnd  37240  totbndbnd  37251  heiborlem3  37275  eliunov2  43081  fvmptiunrelexplb0d  43086  fvmptiunrelexplb1d  43088  comptiunov2i  43108  trclrelexplem  43113  dftrcl3  43122  trclfvcom  43125  cnvtrclfv  43126  cotrcltrcl  43127  trclimalb2  43128  trclfvdecomr  43130  dfrtrcl3  43135  dfrtrcl4  43140  isomenndlem  45890  ovnval  45901  hoicvr  45908  hoicvrrex  45916  ovnlecvr  45918  ovncvrrp  45924  ovnsubaddlem1  45930  hoidmvlelem3  45957  hoidmvle  45960  ovnhoilem1  45961  ovnovollem1  46016  smflimlem3  46133  otiunsndisjX  46631