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

Theorem iuneq1d 4511
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 4500 . 2 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
31, 2syl 17 1 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480   ciun 4485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-v 3188  df-in 3562  df-ss 3569  df-iun 4487
This theorem is referenced by:  iuneq12d  4512  disjxiun  4609  disjxiunOLD  4610  kmlem11  8926  prmreclem4  15547  imasval  16092  iundisj  23223  iundisj2  23224  voliunlem1  23225  iunmbl  23228  volsup  23231  uniioombllem4  23260  iuninc  29224  iundisjf  29247  iundisj2f  29248  iundisjfi  29396  iundisj2fi  29397  iundisjcnt  29398  indval2  29858  sigaclcu3  29966  fiunelros  30018  meascnbl  30063  bnj1113  30564  bnj155  30657  bnj570  30683  bnj893  30706  cvmliftlem10  30984  mrsubvrs  31127  msubvrs  31165  voliunnfl  33085  volsupnfl  33086  heiborlem3  33244  heibor  33252  iunrelexp0  37475  iunp1  38720  iundjiunlem  39983  iundjiun  39984  meaiuninclem  40004  meaiuninc  40005  carageniuncllem1  40042  carageniuncllem2  40043  carageniuncl  40044  caratheodorylem1  40047  caratheodorylem2  40048
  Copyright terms: Public domain W3C validator