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

Theorem iuneq1d 4680
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 4669 . 2 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
31, 2syl 17 1 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631   ciun 4655
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 4657
This theorem is referenced by:  iuneq12d  4681  disjxiun  4784  kmlem11  9188  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  33785  volsupnfl  33786  heiborlem3  33942  heibor  33950  iunrelexp0  38518  iunp1  39754  iundjiunlem  41188  iundjiun  41189  meaiuninclem  41209  meaiuninc  41210  carageniuncllem1  41250  carageniuncllem2  41251  carageniuncl  41252  caratheodorylem1  41255  caratheodorylem2  41256
  Copyright terms: Public domain W3C validator