MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iuneq2d Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 iuneq2d.2 . . 3 (𝜑𝐵 = 𝐶)
21adantr 481 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32iuneq2dv 4976 1 (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106   ciun 4952
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-v 3445  df-in 3915  df-ss 3925  df-iun 4954
This theorem is referenced by:  iununi  5057  oelim2  8534  ituniiun  10316  rtrclreclem1  14902  dfrtrclrec2  14903  rtrclreclem2  14904  rtrclreclem4  14906  imasval  17353  mreacs  17498  cnextval  23364  taylfval  25670  iunpreima  31312  reprdifc  33052  msubvrs  33966  neibastop2  34771  voliunnfl  36060  sstotbnd2  36171  equivtotbnd  36175  totbndbnd  36186  heiborlem3  36210  eliunov2  41862  fvmptiunrelexplb0d  41867  fvmptiunrelexplb1d  41869  comptiunov2i  41889  trclrelexplem  41894  dftrcl3  41903  trclfvcom  41906  cnvtrclfv  41907  cotrcltrcl  41908  trclimalb2  41909  trclfvdecomr  41911  dfrtrcl3  41916  dfrtrcl4  41921  isomenndlem  44672  ovnval  44683  hoicvr  44690  hoicvrrex  44698  ovnlecvr  44700  ovncvrrp  44706  ovnsubaddlem1  44712  hoidmvlelem3  44739  hoidmvle  44742  ovnhoilem1  44743  ovnovollem1  44798  smflimlem3  44915  otiunsndisjX  45412
  Copyright terms: Public domain W3C validator