Theorem iuneq2d 4989

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ ciun 4958

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-v 3452  df-ss 3934  df-iun 4960

This theorem is referenced by:  iununi  5066  oelim2  8562  ituniiun  10382  rtrclreclem1  15030  dfrtrclrec2  15031  rtrclreclem2  15032  rtrclreclem4  15034  imasval  17481  mreacs  17626  pzriprnglem10  21407  cnextval  23955  taylfval  26273  iunpreima  32500  constrlim  33736  reprdifc  34625  msubvrs  35554  neibastop2  36356  voliunnfl  37665  sstotbnd2  37775  equivtotbnd  37779  totbndbnd  37790  heiborlem3  37814  eliunov2  43675  fvmptiunrelexplb0d  43680  fvmptiunrelexplb1d  43682  comptiunov2i  43702  trclrelexplem  43707  dftrcl3  43716  trclfvcom  43719  cnvtrclfv  43720  cotrcltrcl  43721  trclimalb2  43722  trclfvdecomr  43724  dfrtrcl3  43729  dfrtrcl4  43734  isomenndlem  46535  ovnval  46546  hoicvr  46553  hoicvrrex  46561  ovnlecvr  46563  ovncvrrp  46569  ovnsubaddlem1  46575  hoidmvlelem3  46602  hoidmvle  46605  ovnhoilem1  46606  ovnovollem1  46661  smflimlem3  46778  otiunsndisjX  47284