Theorem iuneq2d 4965

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ ciun 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3432  df-ss 3907  df-iun 4936

This theorem is referenced by:  iununi  5042  oelim2  8524  ituniiun  10335  rtrclreclem1  15010  dfrtrclrec2  15011  rtrclreclem2  15012  rtrclreclem4  15014  imasval  17466  mreacs  17615  pzriprnglem10  21480  cnextval  24036  taylfval  26335  iunpreima  32649  constrlim  33899  reprdifc  34787  msubvrs  35758  neibastop2  36559  voliunnfl  37999  sstotbnd2  38109  equivtotbnd  38113  totbndbnd  38124  heiborlem3  38148  eliunov2  44124  fvmptiunrelexplb0d  44129  fvmptiunrelexplb1d  44131  comptiunov2i  44151  trclrelexplem  44156  dftrcl3  44165  trclfvcom  44168  cnvtrclfv  44169  cotrcltrcl  44170  trclimalb2  44171  trclfvdecomr  44173  dfrtrcl3  44178  dfrtrcl4  44183  isomenndlem  46976  ovnval  46987  hoicvr  46994  hoicvrrex  47002  ovnlecvr  47004  ovncvrrp  47010  ovnsubaddlem1  47016  hoidmvlelem3  47043  hoidmvle  47046  ovnhoilem1  47047  ovnovollem1  47102  smflimlem3  47219  otiunsndisjX  47739