Theorem difeq2i 4054

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

Syntax hints:   = wceq 1547   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-dif 3886

This theorem is referenced by:  difeq12i  4055  dfun3  4204  dfin3  4205  dfin4  4206  invdif  4207  indif  4208  difundi  4218  difindi  4220  difdif2  4224  dif32  4230  difabs  4231  dfsymdif3  4234  notrab  4250  dif0  4306  unvdif  4403  difdifdir  4419  dfif3  4469  difpr  4736  iinvdif  5009  cnvin  6095  fndifnfp  7120  dif1o  8425  dfsdom2  9028  brttrcl2  9626  ttrcltr  9628  rnttrcl  9634  dju1dif  10086  m1bits  16400  clsval2  23033  mretopd  23075  cmpfi  23391  llycmpkgen2  23533  pserdvlem2  26411  nbgrssvwo2  29449  finsumvtxdg2ssteplem1  29632  frgrwopreglem3  30402  iundifdifd  32650  iundifdif  32651  difres  32689  gsumhashmul  33148  pmtrcnelor  33172  cycpmconjv  33223  cyc3conja  33238  elrgspnsubrunlem2  33329  evlextv  33726  sibfof  34524  eulerpartlemmf  34559  fineqvnttrclselem1  35302  kur14lem2  35435  kur14lem6  35439  kur14lem7  35440  satfv1  35591  dfon4  36119  onint1  36677  bj-2upln1upl  37377  poimirlem8  37995  dmcnvep  38755  dfssr2  38946  prjspval2  43063  diophren  43258  ordeldif1o  43705  nonrel  44028  dssmapntrcls  44572  salincl  46767  meaiuninc  46924  carageniuncllem1  46964  iscnrm3rlem3  49432