Theorem difeq1i 4095

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

Syntax hints:   = wceq 1537   ∖ cdif 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-dif 3939

This theorem is referenced by:  difeq12i  4097  dfin3  4243  indif1  4248  indifcom  4249  difun1  4264  notab  4273  notrab  4280  undifabs  4426  difprsn1  4733  difprsn2  4734  diftpsn3  4735  resdifcom  5872  resdmdfsn  5901  wfi  6181  orddif  6284  fresaun  6549  f12dfv  7030  f13dfv  7031  domunsncan  8617  phplem1  8696  elfiun  8894  dju1dif  9598  axcclem  9879  dfn2  11911  mvdco  18573  pmtrdifellem2  18605  islinds2  20957  lindsind2  20963  restcld  21780  ufprim  22517  volun  24146  itgsplitioo  24438  uhgr0vb  26857  uhgr0  26858  uvtxupgrres  27190  cplgr3v  27217  ex-dif  28202  indifundif  30285  imadifxp  30351  aciunf1  30408  pmtrcnelor  30735  lindsunlem  31020  lindsun  31021  braew  31501  carsgclctunlem1  31575  carsggect  31576  coinflippvt  31742  ballotlemfval0  31753  signstfvcl  31843  satf0  32619  frpoind  33080  frind  33085  onint1  33797  bj-2upln1upl  34339  bj-disj2r  34343  lindsenlbs  34902  poimirlem13  34920  poimirlem14  34921  poimirlem18  34925  poimirlem21  34928  poimirlem30  34937  itg2addnclem  34958  asindmre  34992  rabdif  39156  kelac2  39714  fourierdlem102  42542  fourierdlem114  42554  pwsal  42649  issald  42665  sge0fodjrnlem  42747  hoiprodp1  42919  lincext2  44559