Theorem difeq2i 4078

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 4075	. 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  dfun3  4229  dfin3  4230  dfin4  4231  invdif  4232  indif  4233  difundi  4243  difindi  4245  difdif2  4249  dif32  4255  difabs  4256  dfsymdif3  4259  notrab  4275  dif0  4334  unvdif  4436  difdifdir  4452  dfif3  4502  difpr  4771  iinvdif  5046  cnvin  6141  fndifnfp  7174  dif1o  8481  dfsdom2  9084  brttrcl2  9679  ttrcltr  9681  rnttrcl  9687  dju1dif  10152  m1bits  16493  clsval2  23207  mretopd  23249  cmpfi  23565  llycmpkgen2  23707  pserdvlem2  26591  nbgrssvwo2  29712  finsumvtxdg2ssteplem1  29895  frgrwopreglem3  30665  iundifdifd  32906  iundifdif  32907  difres  32945  gsumhashmul  33387  pmtrcnelor  33411  cycpmconjv  33462  cyc3conja  33477  elrgspnsubrunlem2  33568  evlextv  33932  sibfof  34730  eulerpartlemmf  34765  fineqvnttrclselem1  35534  kur14lem2  35699  kur14lem6  35703  kur14lem7  35704  satfv1  35855  dfon4  36383  onint1  36960  bj-2upln1upl  37660  poimirlem8  38279  dmcnvep  39037  dfssr2  39228  prjspval2  43345  diophren  43540  ordeldif1o  43987  nonrel  44310  dssmapntrcls  44854  salincl  47038  meaiuninc  47195  carageniuncllem1  47235  iscnrm3rlem3  49720