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 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  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  8538  ituniiun  10354  rtrclreclem1  14934  dfrtrclrec2  14935  rtrclreclem2  14936  rtrclreclem4  14938  imasval  17385  mreacs  17530  cnextval  23396  taylfval  25702  iunpreima  31369  reprdifc  33109  msubvrs  34023  neibastop2  34800  voliunnfl  36089  sstotbnd2  36200  equivtotbnd  36204  totbndbnd  36215  heiborlem3  36239  eliunov2  41893  fvmptiunrelexplb0d  41898  fvmptiunrelexplb1d  41900  comptiunov2i  41920  trclrelexplem  41925  dftrcl3  41934  trclfvcom  41937  cnvtrclfv  41938  cotrcltrcl  41939  trclimalb2  41940  trclfvdecomr  41942  dfrtrcl3  41947  dfrtrcl4  41952  isomenndlem  44703  ovnval  44714  hoicvr  44721  hoicvrrex  44729  ovnlecvr  44731  ovncvrrp  44737  ovnsubaddlem1  44743  hoidmvlelem3  44770  hoidmvle  44773  ovnhoilem1  44774  ovnovollem1  44829  smflimlem3  44946  otiunsndisjX  45443
  Copyright terms: Public domain W3C validator