Theorem difeq1d 4078

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 4072	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Syntax hints:   → wi 4   = wceq 1540   ∖ cdif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-dif 3908

This theorem is referenced by:  difeq12d  4080  dffv2  6922  on2recsov  8593  phplem2  9129  unfilem3  9214  marypha1lem  9342  infdifsn  9572  cantnfp1lem3  9595  en2other2  9922  isacn  9957  fin23lem28  10253  enfin1ai  10297  fin1a2lem7  10319  fzdifsuc  13505  axdc4uz  13909  leiso  14384  cshimadifsn  14754  isstruct2  17078  strle1  17087  setsfun0  17101  pltfval  18253  f1omvdco2  19345  symgsssg  19364  symgfisg  19365  symggen  19367  pmtrdifellem3  19375  pmtrdifwrdellem3  19380  pmtrdifwrdel2lem1  19381  pmtrdifwrdel  19382  pmtrdifwrdel2  19383  psgnunilem1  19390  psgnunilem5  19391  psgnunilem2  19392  psgnunilem3  19393  gsumval3  19804  dmdprd  19897  dprd2da  19941  dmdprdsplit2lem  19944  dpjfval  19954  ablfac1eulem  19971  subdrgint  20706  lssset  20854  lbspropd  21021  islindf  21737  islindf2  21739  f1lindf  21747  opsrtoslem2  21979  cldval  22926  difopn  22937  mretopd  22995  restcld  23075  ordtcld1  23100  ordtcld2  23101  cnclima  23171  iscncl  23172  isreg2  23280  llycmpkgen2  23453  1stckgen  23457  ptval  23473  txcld  23506  ptcld  23516  txkgen  23555  qtopcld  23616  qtoprest  23620  qtopcmap  23622  kqcldsat  23636  regr1lem  23642  trufil  23813  ufildr  23834  opnsubg  24011  cldsubg  24014  blcld  24409  lebnumlem1  24876  bcthlem1  25240  bcth  25245  bcth3  25247  difmbl  25460  itg1val  25600  itgioo  25733  limciun  25811  dvfval  25814  newval  27783  noxpordpred  27883  istrkgl  28421  ishpg  28722  eengv  28942  elntg  28947  isuhgr  29023  isushgr  29024  uhgreq12g  29028  isuhgrop  29033  uhgr0vb  29035  uhgrun  29037  uhgrstrrepe  29041  isupgr  29047  upgrop  29057  isumgr  29058  upgrun  29081  isuspgr  29115  isusgr  29116  isuspgrop  29124  nb3grprlem2  29344  uvtxval  29350  nbupgruvtxres  29370  cplgrop  29400  cusgrexi  29406  structtocusgr  29409  1loopgrnb0  29466  cyclnumvtx  29763  isconngr1  30152  frgr3v  30237  difuncomp  32515  imadifxp  32563  fressupp  32644  supppreima  32647  mptiffisupp  32649  gtiso  32657  difico  32739  fzdif2  32746  fzodif2  32747  fzodif1  32748  ischn  32961  chnind  32966  chnccats1  32970  pmtrcnel2  33045  cycpmconjvlem  33096  cycpmrn  33098  tocyccntz  33099  submarchi  33141  elrgspnlem4  33198  fracfld  33260  elrspunidl  33378  qtophaus  33805  imambfm  34232  difelcarsg  34280  carsgclctunlem1  34287  carsggect  34288  issibf  34303  sibf0  34304  sitgfval  34311  ballotlemfval  34460  ballotlemfp1  34462  ballotlemgun  34495  hgt750lemb  34626  kur14  35191  iscvm  35234  cvmscld  35248  satf  35328  mdvval  35479  topbnd  36300  pibp21  37391  poimirlem2  37604  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem11  37613  poimirlem12  37614  poimirlem13  37615  poimirlem14  37616  poimirlem16  37618  poimirlem18  37620  poimirlem19  37621  poimirlem21  37623  poimirlem22  37624  poimirlem23  37625  poimirlem27  37629  poimirlem30  37632  mblfinlem3  37641  mblfinlem4  37642  itg2addnclem  37653  itg2addnclem2  37654  prjspeclsp  42588  aomclem8  43037  kelac2  43041  gneispace2  44108  fzdifsuc2  45295  iccdifioo  45500  iccdifprioo  45501  ibliooicc  45956  dirkercncflem2  46089  issal  46299  prsal  46303  saldifcl2  46313  intsal  46315  sge0fodjrnlem  46401  caratheodorylem1  46511  vonvolmbllem  46645  salpreimagelt  46692  salpreimalegt  46694  smfresal  46773  dfnbgr5  47839  dfnbgr6  47845  isubgruhgr  47856  stgrnbgr0  47952  lines  48720  rrxlines  48722  eenglngeehlnm  48728  clddisj  48892  iscnrm3rlem1  48928