Theorem difeq2i 4077

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

Syntax hints:   = wceq 1560   ∖ cdif 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-dif 3907

This theorem is referenced by:  difeq12i  4078  dfun3  4228  dfin3  4229  dfin4  4230  invdif  4231  indif  4232  difundi  4242  difindi  4244  difdif2  4248  dif32  4254  difabs  4255  dfsymdif3  4258  notrab  4274  dif0  4331  unvdif  4429  difdifdir  4445  dfif3  4495  difpr  4763  iinvdif  5037  cnvin  6128  fndifnfp  7160  dif1o  8469  dfsdom2  9072  brttrcl2  9669  ttrcltr  9671  rnttrcl  9677  dju1dif  10129  m1bits  16474  clsval2  23107  mretopd  23149  cmpfi  23465  llycmpkgen2  23607  pserdvlem2  26488  nbgrssvwo2  29560  finsumvtxdg2ssteplem1  29743  frgrwopreglem3  30513  iundifdifd  32758  iundifdif  32759  difres  32797  gsumhashmul  33244  pmtrcnelor  33268  cycpmconjv  33319  cyc3conja  33334  elrgspnsubrunlem2  33426  evlextv  33836  sibfof  34634  eulerpartlemmf  34669  fineqvnttrclselem1  35414  kur14lem2  35554  kur14lem6  35558  kur14lem7  35559  satfv1  35710  dfon4  36238  onint1  36806  bj-2upln1upl  37506  poimirlem8  38124  dmcnvep  38884  dfssr2  39075  prjspval2  43192  diophren  43387  ordeldif1o  43834  nonrel  44157  dssmapntrcls  44701  salincl  46895  meaiuninc  47052  carageniuncllem1  47092  iscnrm3rlem3  49560