Theorem iuneq2d 5022

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∪ ciun 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-iun 4993

This theorem is referenced by:  iununi  5099  oelim2  8633  ituniiun  10462  rtrclreclem1  15096  dfrtrclrec2  15097  rtrclreclem2  15098  rtrclreclem4  15100  imasval  17556  mreacs  17701  pzriprnglem10  21501  cnextval  24069  taylfval  26400  iunpreima  32577  constrlim  33780  reprdifc  34642  msubvrs  35565  neibastop2  36362  voliunnfl  37671  sstotbnd2  37781  equivtotbnd  37785  totbndbnd  37796  heiborlem3  37820  eliunov2  43692  fvmptiunrelexplb0d  43697  fvmptiunrelexplb1d  43699  comptiunov2i  43719  trclrelexplem  43724  dftrcl3  43733  trclfvcom  43736  cnvtrclfv  43737  cotrcltrcl  43738  trclimalb2  43739  trclfvdecomr  43741  dfrtrcl3  43746  dfrtrcl4  43751  isomenndlem  46545  ovnval  46556  hoicvr  46563  hoicvrrex  46571  ovnlecvr  46573  ovncvrrp  46579  ovnsubaddlem1  46585  hoidmvlelem3  46612  hoidmvle  46615  ovnhoilem1  46616  ovnovollem1  46671  smflimlem3  46788  otiunsndisjX  47291