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

Theorem iuneq1d 4981
Description: Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
Hypothesis
Ref Expression
iuneq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
iuneq1d (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq1d
StepHypRef Expression
1 iuneq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 iuneq1 4970 . 2 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
31, 2syl 17 1 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541   ciun 4954
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-rex 3074  df-v 3447  df-in 3917  df-ss 3927  df-iun 4956
This theorem is referenced by:  iuneq12d  4982  disjxiun  5102  kmlem11  10096  prmreclem4  16791  imasval  17393  iundisj  24912  iundisj2  24913  voliunlem1  24914  iunmbl  24917  volsup  24920  uniioombllem4  24950  iuninc  31479  iundisjf  31507  iundisj2f  31508  suppovss  31598  iundisjfi  31699  iundisj2fi  31700  iundisjcnt  31701  indval2  32613  sigaclcu3  32721  fiunelros  32773  meascnbl  32818  bnj1113  33397  bnj155  33491  bnj570  33517  bnj893  33540  cvmliftlem10  33888  mrsubvrs  34116  msubvrs  34154  voliunnfl  36122  volsupnfl  36123  heiborlem3  36272  heibor  36280  iunrelexp0  41964  iunp1  43264  iundjiunlem  44690  iundjiun  44691  meaiuninclem  44711  meaiuninc  44712  carageniuncllem1  44752  carageniuncllem2  44753  carageniuncl  44754  caratheodorylem1  44757  caratheodorylem2  44758
  Copyright terms: Public domain W3C validator