Theorem iuneq2d 4981

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3453  df-ss 3916  df-iun 4953

This theorem is used by:  iununi  5059  iunpreima  7066  oelim2  8597  ituniiun  10493  rtrclreclem1  15203  dfrtrclrec2  15204  rtrclreclem2  15205  rtrclreclem4  15207  imasval  17676  mreacs  17825  pzriprnglem10  21789  cnextval  24373  taylfval  26679  constrlim  34364  reprdifc  35249  msubvrs  36304  nmulprop  36919  neibastop2  37129  voliunnfl  38562  sstotbnd2  38688  equivtotbnd  38692  totbndbnd  38703  heiborlem3  38727  eliunov2  44664  fvmptiunrelexplb0d  44669  fvmptiunrelexplb1d  44671  comptiunov2i  44691  trclrelexplem  44696  dftrcl3  44705  trclfvcom  44708  cnvtrclfv  44709  cotrcltrcl  44710  trclimalb2  44711  trclfvdecomr  44713  dfrtrcl3  44718  dfrtrcl4  44723  isomenndlem  47509  ovnval  47520  hoicvr  47527  hoicvrrex  47535  ovnlecvr  47537  ovncvrrp  47543  ovnsubaddlem1  47549  hoidmvlelem3  47576  hoidmvle  47579  ovnhoilem1  47580  ovnovollem1  47635  smflimlem3  47752  otiunsndisjX  48318