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

Theorem difeq2d 4096
Description: Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
difeq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem difeq2d
StepHypRef Expression
1 difeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 difeq2 4090 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cdif 3930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rab 3144  df-dif 3936
This theorem is referenced by:  difeq12d  4097  iinvdif  4993  otiunsndisj  5401  xpdifid  6018  imain  6432  dffv2  6749  f12dfv  7021  f13dfv  7022  tz7.49  8070  oev2  8137  difsnen  8587  domunsncan  8605  sbthlem2  8616  sbthlem3  8617  sbth  8625  phplem3  8686  phplem4  8687  unblem2  8759  unblem3  8760  xpfi  8777  dfac8alem  9443  dfac8a  9444  kmlem9  9572  kmlem11  9574  kmlem12  9575  compsscnvlem  9780  s3iunsndisj  14316  isercolllem3  15011  ruclem13  15583  bitsf1  15783  setsvalg  16500  setsval  16501  setsdm  16505  ismri2dad  16896  mreexmrid  16902  mreexexlemd  16903  gsumvalx  17874  gsumpropd  17876  gsumpropd2lem  17877  gsumress  17880  pmtrfv  18509  gsumval3a  18952  gsumval3  18956  dprdcntz  19059  dprddisj  19060  dprdsn  19087  dprddisj2  19090  dpjval  19107  ablfac1eu  19124  drngprop  19442  subdrgint  19511  lbsind  19781  islbs2  19855  lbsextlem4  19862  lbsextg  19863  frlmlbs  20869  lindfind  20888  lindsind  20889  lindfrn  20893  f1lindf  20894  submaval  21118  mdetunilem3  21151  mdetunilem4  21152  mdetunilem9  21157  clsval2  21586  ntrval2  21587  ntrdif  21588  clsdif  21589  cmclsopn  21598  islp  21676  pnrmopn  21879  hauscmplem  21942  bwth  21946  conndisj  21952  cvsunit  23662  bcthlem1  23854  bcth  23859  bcth3  23861  cmmbl  24062  nulmbl2  24064  shftmbl  24066  volsup  24084  mbfimaicc  24159  eldv  24423  ig1pval  24693  tglngval  26264  axlowdimlem15  26669  axlowdim  26674  nbgr2vtx1edg  27059  nbuhgr2vtx1edgb  27061  nb3grprlem2  27090  uvtxel  27097  uvtxel1  27105  uvtxusgrel  27112  cusgredg  27133  cplgr1v  27139  cplgr3v  27144  usgredgsscusgredg  27168  usgr2pthlem  27471  2wspiundisj  27669  frcond1  27972  frgr1v  27977  nfrgr2v  27978  frgr3v  27981  1vwmgr  27982  3vfriswmgr  27984  3cyclfrgrrn1  27991  n4cyclfrgr  27997  frgrwopreglem4a  28016  odpmco  30657  tocycfv  30678  tocycf  30686  tocyc01  30687  cycpm2tr  30688  cycpmconjslem2  30724  cyc3conja  30726  0nellinds  30862  lindssn  30866  lbslsat  30913  lindsunlem  30919  sigapildsyslem  31319  carsgclctunlem3  31477  sitgval  31489  ballotlemfval  31646  cplgredgex  32264  cvmscbv  32402  cvmsdisj  32414  cvmsss2  32418  satfv1  32507  satffunlem  32545  satffunlem1lem1  32546  satffunlem2lem1  32548  clsun  33573  lindsadd  34766  lindsenlbs  34768  poimirlem25  34798  poimirlem26  34799  poimirlem27  34800  cnambfre  34821  watvalN  37009  dnnumch1  39522  aomclem3  39534  aomclem8  39539  dssmapfv2d  40242  dssmapfv3d  40243  dssmapnvod  40244  clsk3nimkb  40268  ntrclscls00  40294  ntrclsiso  40295  ntrclsk3  40298  ntrclsk4  40300  nzprmdif  40528  compne  40650  dvmptfprodlem  42105  fouriercn  42394  meaiininclem  42645  meaiininc  42646  carageniuncllem1  42680  lindslinindsimp2  44446  ldepsnlinc  44491  line  44647  rrxline  44649
  Copyright terms: Public domain W3C validator