Theorem iuneq2d 4483

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-iun 4457

This theorem is referenced by:  iununi  4546  oelim2  7562  ituniiun  9127  dfrtrclrec2  13645  rtrclreclem1  13646  rtrclreclem2  13647  rtrclreclem4  13649  imasval  15994  mreacs  16142  cnextval  21675  taylfval  23917  iunpreima  28765  msubvrs  30711  trpredeq1  30964  trpredeq2  30965  neibastop2  31526  voliunnfl  32623  sstotbnd2  32743  equivtotbnd  32747  totbndbnd  32758  heiborlem3  32782  eliunov2  36990  fvmptiunrelexplb0d  36995  fvmptiunrelexplb1d  36997  comptiunov2i  37017  trclrelexplem  37022  dftrcl3  37031  trclfvcom  37034  cnvtrclfv  37035  cotrcltrcl  37036  trclimalb2  37037  trclfvdecomr  37039  dfrtrcl3  37044  dfrtrcl4  37049  isomenndlem  39420  ovnval  39431  hoicvr  39438  hoicvrrex  39446  ovnlecvr  39448  ovncvrrp  39454  ovnsubaddlem1  39460  hoidmvlelem3  39487  hoidmvle  39490  ovnhoilem1  39491  ovnovollem1  39546  smflimlem3  39659  otiunsndisjX  40317