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

Theorem iuneq1d 4909
 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 4898 . 2 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
31, 2syl 17 1 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  ∪ ciun 4882 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-in 3888  df-ss 3898  df-iun 4884 This theorem is referenced by:  iuneq12d  4910  disjxiun  5028  kmlem11  9574  prmreclem4  16248  imasval  16779  iundisj  24162  iundisj2  24163  voliunlem1  24164  iunmbl  24167  volsup  24170  uniioombllem4  24200  iuninc  30334  iundisjf  30362  iundisj2f  30363  suppovss  30453  iundisjfi  30555  iundisj2fi  30556  iundisjcnt  30557  indval2  31398  sigaclcu3  31506  fiunelros  31558  meascnbl  31603  bnj1113  32182  bnj155  32276  bnj570  32302  bnj893  32325  cvmliftlem10  32669  mrsubvrs  32897  msubvrs  32935  voliunnfl  35120  volsupnfl  35121  heiborlem3  35270  heibor  35278  iunrelexp0  40446  iunp1  41743  iundjiunlem  43141  iundjiun  43142  meaiuninclem  43162  meaiuninc  43163  carageniuncllem1  43203  carageniuncllem2  43204  carageniuncl  43205  caratheodorylem1  43208  caratheodorylem2  43209
 Copyright terms: Public domain W3C validator