Theorem difeq2i 4050

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

Syntax hints:   = wceq 1539   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-dif 3886

This theorem is referenced by:  difeq12i  4051  dfun3  4196  dfin3  4197  dfin4  4198  invdif  4199  indif  4200  difundi  4210  difindi  4212  difdif2  4217  dif32  4223  difabs  4224  dfsymdif3  4227  notrab  4242  dif0  4303  unvdif  4405  difdifdir  4419  dfif3  4470  difpr  4733  iinvdif  5005  cnvin  6037  fndifnfp  7030  dif1o  8292  dfsdom2  8836  dju1dif  9859  m1bits  16075  clsval2  22109  mretopd  22151  cmpfi  22467  llycmpkgen2  22609  pserdvlem2  25492  nbgrssvwo2  27632  finsumvtxdg2ssteplem1  27815  frgrwopreglem3  28579  iundifdifd  30802  iundifdif  30803  difres  30840  gsumhashmul  31218  pmtrcnelor  31262  cycpmconjv  31311  cyc3conja  31326  sibfof  32207  eulerpartlemmf  32242  kur14lem2  33069  kur14lem6  33073  kur14lem7  33074  satfv1  33225  brttrcl2  33700  ttrcltr  33702  rnttrcl  33708  dfon4  34122  onint1  34565  bj-2upln1upl  35141  poimirlem8  35712  dfssr2  36544  prjspval2  40373  diophren  40551  nonrel  41081  dssmapntrcls  41627  salincl  43754  meaiuninc  43909  carageniuncllem1  43949  iscnrm3rlem3  46124