Theorem difeq2i 4064

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

Hypothesis

Ref	Expression
difeq1i.1	⊢ 𝐴 = 𝐵

Assertion

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

Proof of Theorem difeq2i

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

Syntax hints:   = wceq 1542   ∖ cdif 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-dif 3893

This theorem is referenced by:  difeq12i  4065  dfun3  4217  dfin3  4218  dfin4  4219  invdif  4220  indif  4221  difundi  4231  difindi  4233  difdif2  4237  dif32  4243  difabs  4244  dfsymdif3  4247  notrab  4263  dif0  4319  unvdif  4416  difdifdir  4432  dfif3  4482  difpr  4747  iinvdif  5023  cnvin  6103  fndifnfp  7125  dif1o  8429  dfsdom2  9032  brttrcl2  9629  ttrcltr  9631  rnttrcl  9637  dju1dif  10089  m1bits  16403  clsval2  23028  mretopd  23070  cmpfi  23386  llycmpkgen2  23528  pserdvlem2  26409  nbgrssvwo2  29448  finsumvtxdg2ssteplem1  29632  frgrwopreglem3  30402  iundifdifd  32649  iundifdif  32650  difres  32688  gsumhashmul  33146  pmtrcnelor  33170  cycpmconjv  33221  cyc3conja  33236  elrgspnsubrunlem2  33327  evlextv  33704  sibfof  34503  eulerpartlemmf  34538  fineqvnttrclselem1  35284  kur14lem2  35408  kur14lem6  35412  kur14lem7  35413  satfv1  35564  dfon4  36092  onint1  36650  bj-2upln1upl  37350  poimirlem8  37966  dmcnvep  38726  dfssr2  38917  prjspval2  43063  diophren  43262  ordeldif1o  43709  nonrel  44032  dssmapntrcls  44576  salincl  46773  meaiuninc  46930  carageniuncllem1  46970  iscnrm3rlem3  49432