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

Theorem iuneq1d 4701
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 4690 . 2 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
31, 2syl 17 1 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652   ciun 4676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-v 3352  df-in 3739  df-ss 3746  df-iun 4678
This theorem is referenced by:  iuneq12d  4702  disjxiun  4806  kmlem11  9235  prmreclem4  15904  imasval  16439  iundisj  23606  iundisj2  23607  voliunlem1  23608  iunmbl  23611  volsup  23614  uniioombllem4  23644  iuninc  29762  iundisjf  29785  iundisj2f  29786  iundisjfi  29939  iundisj2fi  29940  iundisjcnt  29941  indval2  30458  sigaclcu3  30567  fiunelros  30619  meascnbl  30664  bnj1113  31236  bnj155  31329  bnj570  31355  bnj893  31378  cvmliftlem10  31656  mrsubvrs  31799  msubvrs  31837  voliunnfl  33809  volsupnfl  33810  heiborlem3  33966  heibor  33974  iunrelexp0  38601  iunp1  39818  iundjiunlem  41245  iundjiun  41246  meaiuninclem  41266  meaiuninc  41267  carageniuncllem1  41307  carageniuncllem2  41308  carageniuncl  41309  caratheodorylem1  41312  caratheodorylem2  41313
  Copyright terms: Public domain W3C validator