Theorem difeq1i 4114

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 4111	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)

Syntax hints:   = wceq 1534   ∖ cdif 3941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-dif 3947

This theorem is referenced by:  difeq12i  4116  dfin3  4262  indif1  4267  indifcom  4268  difun1  4285  notab  4300  notrab  4307  undifabs  4473  difprsn1  4799  difprsn2  4800  diftpsn3  4801  resdifcom  5998  resdmdfsn  6029  frpoind  6342  wfiOLD  6351  orddif  6459  fresaun  6762  f12dfv  7276  f13dfv  7277  domunsncan  9090  phplem1OLD  9235  elfiun  9447  frind  9767  dju1dif  10189  axcclem  10474  dfn2  12509  mvdco  19393  pmtrdifellem2  19425  islinds2  21740  lindsind2  21746  restcld  23069  ufprim  23806  volun  25467  itgsplitioo  25760  uhgr0vb  28878  uhgr0  28879  uvtxupgrres  29214  cplgr3v  29241  ex-dif  30226  indifundif  32314  imadifxp  32384  aciunf1  32442  pmtrcnelor  32808  lindsunlem  33308  lindsun  33309  braew  33851  carsgclctunlem1  33927  carsggect  33928  coinflippvt  34094  ballotlemfval0  34105  signstfvcl  34195  satf0  34972  onint1  35923  bj-2upln1upl  36493  bj-disj2r  36497  lindsenlbs  37077  poimirlem13  37095  poimirlem14  37096  poimirlem18  37100  poimirlem21  37103  poimirlem30  37112  itg2addnclem  37133  asindmre  37165  sucdifsn  37698  disjresundif  37702  ressucdifsn  37704  rabdif  41675  kelac2  42461  fourierdlem102  45568  fourierdlem114  45580  pwsal  45675  issald  45693  sge0fodjrnlem  45776  hoiprodp1  45948  lincext2  47495  disjdifb  47852