Theorem difeq1i 4077

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

Hypothesis

Ref	Expression
difeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
difeq1i	⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)

Proof of Theorem difeq1i

Step	Hyp	Ref	Expression
1		difeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		difeq1 4074	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)

Syntax hints:   = wceq 1570   ∖ cdif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-dif 3908

This theorem is referenced by:  difeq12i  4079  dfin3  4230  indif1  4235  indifcom  4236  difun1  4252  notab  4267  rabdif  4274  notrab  4275  undifabs  4439  difprsn1  4768  difprsn2  4769  diftpsn3  4770  resdifcom  5997  resdmdfsn  6031  resdmdfsnOLD  6032  frpoind  6343  orddif  6459  fresaun  6749  f12dfv  7271  f13dfv  7272  domunsncan  9061  elfiun  9386  frind  9718  dju1dif  10152  axcclem  10436  dfn2  12512  nulchn  18670  s1chn  18671  chnccat  18677  ex-chn1  18688  ex-chn2  18689  mvdco  19510  pmtrdifellem2  19542  islinds2  21963  lindsind2  21969  restcld  23329  ufprim  24066  volun  25704  itgsplitioo  25997  uhgr0vb  29422  uhgr0  29423  uvtxupgrres  29758  cplgr3v  29785  ex-dif  30774  indifundif  32870  imadifxp  32946  aciunf1  33008  indsupp  33187  pmtrcnelor  33411  lindsunlem  34014  lindsun  34015  braew  34632  carsgclctunlem1  34707  carsggect  34708  coinflippvt  34875  ballotlemfval0  34886  signstfvcl  34960  satf0  35864  onint1  36960  bj-2upln1upl  37660  bj-disj2r  37664  lindsenlbs  38266  poimirlem13  38284  poimirlem14  38285  poimirlem18  38289  poimirlem21  38292  poimirlem30  38301  itg2addnclem  38322  asindmre  38354  disjresundif  38895  dmxrnuncnvepres  39041  dmxrncnvepres2  39082  sucdifsn  39135  ressucdifsn  39137  kelac2  43792  fourierdlem102  46922  fourierdlem114  46934  pwsal  47029  issald  47047  sge0fodjrnlem  47130  hoiprodp1  47302  lincext2  49235  disjdifb  49588