Theorem difeq1d 4148

Description: Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
difeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
difeq1d	⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Proof of Theorem difeq1d

Step	Hyp	Ref	Expression
1		difeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		difeq1 4142	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Syntax hints:   → wi 4   = wceq 1537   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-dif 3979

This theorem is referenced by:  difeq12d  4150  dffv2  7017  on2recsov  8724  phplem2  9271  phplem4OLD  9283  unfilem3  9373  marypha1lem  9502  infdifsn  9726  cantnfp1lem3  9749  en2other2  10078  isacn  10113  fin23lem28  10409  enfin1ai  10453  fin1a2lem7  10475  fzdifsuc  13644  axdc4uz  14035  leiso  14508  cshimadifsn  14878  isstruct2  17196  strle1  17205  setsfun0  17219  pltfval  18401  f1omvdco2  19490  symgsssg  19509  symgfisg  19510  symggen  19512  pmtrdifellem3  19520  pmtrdifwrdellem3  19525  pmtrdifwrdel2lem1  19526  pmtrdifwrdel  19527  pmtrdifwrdel2  19528  psgnunilem1  19535  psgnunilem5  19536  psgnunilem2  19537  psgnunilem3  19538  gsumval3  19949  dmdprd  20042  dprd2da  20086  dmdprdsplit2lem  20089  dpjfval  20099  ablfac1eulem  20116  subdrgint  20826  lssset  20954  lbspropd  21121  islindf  21855  islindf2  21857  f1lindf  21865  opsrtoslem2  22103  cldval  23052  difopn  23063  mretopd  23121  restcld  23201  ordtcld1  23226  ordtcld2  23227  cnclima  23297  iscncl  23298  isreg2  23406  llycmpkgen2  23579  1stckgen  23583  ptval  23599  txcld  23632  ptcld  23642  txkgen  23681  qtopcld  23742  qtoprest  23746  qtopcmap  23748  kqcldsat  23762  regr1lem  23768  trufil  23939  ufildr  23960  opnsubg  24137  cldsubg  24140  blcld  24539  lebnumlem1  25012  bcthlem1  25377  bcth  25382  bcth3  25384  difmbl  25597  itg1val  25737  itgioo  25871  limciun  25949  dvfval  25952  newval  27912  noxpordpred  28004  istrkgl  28484  ishpg  28785  eengv  29012  elntg  29017  isuhgr  29095  isushgr  29096  uhgreq12g  29100  isuhgrop  29105  uhgr0vb  29107  uhgrun  29109  uhgrstrrepe  29113  isupgr  29119  upgrop  29129  isumgr  29130  upgrun  29153  isuspgr  29187  isusgr  29188  isuspgrop  29196  nb3grprlem2  29416  uvtxval  29422  nbupgruvtxres  29442  cplgrop  29472  cusgrexi  29478  structtocusgr  29481  1loopgrnb0  29538  isconngr1  30222  frgr3v  30307  difuncomp  32576  imadifxp  32623  fressupp  32700  supppreima  32703  mptiffisupp  32705  gtiso  32712  difico  32788  fzdif2  32796  fzodif2  32797  fzodif1  32798  ischn  32979  chnind  32983  pmtrcnel2  33083  cycpmconjvlem  33134  cycpmrn  33136  tocyccntz  33137  submarchi  33166  fracfld  33275  elrspunidl  33421  qtophaus  33782  imambfm  34227  difelcarsg  34275  carsgclctunlem1  34282  carsggect  34283  issibf  34298  sibf0  34299  sitgfval  34306  ballotlemfval  34454  ballotlemfp1  34456  ballotlemgun  34489  hgt750lemb  34633  kur14  35184  iscvm  35227  cvmscld  35241  satf  35321  mdvval  35472  topbnd  36290  pibp21  37381  poimirlem2  37582  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem16  37596  poimirlem18  37598  poimirlem19  37599  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem27  37607  poimirlem30  37610  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem  37631  itg2addnclem2  37632  prjspeclsp  42567  aomclem8  43018  kelac2  43022  gneispace2  44094  fzdifsuc2  45225  iccdifioo  45433  iccdifprioo  45434  ibliooicc  45892  dirkercncflem2  46025  issal  46235  prsal  46239  saldifcl2  46249  intsal  46251  sge0fodjrnlem  46337  caratheodorylem1  46447  vonvolmbllem  46581  salpreimagelt  46628  salpreimalegt  46630  smfresal  46709  dfnbgr5  47723  dfnbgr6  47729  isubgruhgr  47738  lines  48465  rrxlines  48467  eenglngeehlnm  48473  clddisj  48583  iscnrm3rlem1  48620