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

Theorem iuneq1d 4679
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 4668 . 2 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
31, 2syl 17 1 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631   ciun 4654
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-in 3730  df-ss 3737  df-iun 4656
This theorem is referenced by:  iuneq12d  4680  disjxiun  4783  kmlem11  9184  prmreclem4  15830  imasval  16379  iundisj  23536  iundisj2  23537  voliunlem1  23538  iunmbl  23541  volsup  23544  uniioombllem4  23574  iuninc  29717  iundisjf  29740  iundisj2f  29741  iundisjfi  29895  iundisj2fi  29896  iundisjcnt  29897  indval2  30416  sigaclcu3  30525  fiunelros  30577  meascnbl  30622  bnj1113  31194  bnj155  31287  bnj570  31313  bnj893  31336  cvmliftlem10  31614  mrsubvrs  31757  msubvrs  31795  voliunnfl  33786  volsupnfl  33787  heiborlem3  33944  heibor  33952  iunrelexp0  38520  iunp1  39756  iundjiunlem  41193  iundjiun  41194  meaiuninclem  41214  meaiuninc  41215  carageniuncllem1  41255  carageniuncllem2  41256  carageniuncl  41257  caratheodorylem1  41260  caratheodorylem2  41261
  Copyright terms: Public domain W3C validator