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 1542   ∖ cdif 3900

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 3402  df-dif 3906

This theorem is referenced by:  difeq12i  4078  dfun3  4230  dfin3  4231  dfin4  4232  invdif  4233  indif  4234  difundi  4244  difindi  4246  difdif2  4250  dif32  4256  difabs  4257  dfsymdif3  4260  notrab  4276  dif0  4332  unvdif  4429  difdifdir  4446  dfif3  4496  difpr  4761  iinvdif  5037  cnvin  6110  fndifnfp  7132  dif1o  8437  dfsdom2  9040  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  dju1dif  10095  m1bits  16379  clsval2  23006  mretopd  23048  cmpfi  23364  llycmpkgen2  23506  pserdvlem2  26406  nbgrssvwo2  29447  finsumvtxdg2ssteplem1  29631  frgrwopreglem3  30401  iundifdifd  32648  iundifdif  32649  difres  32687  gsumhashmul  33161  pmtrcnelor  33185  cycpmconjv  33236  cyc3conja  33251  elrgspnsubrunlem2  33342  evlextv  33719  sibfof  34518  eulerpartlemmf  34553  fineqvnttrclselem1  35299  kur14lem2  35423  kur14lem6  35427  kur14lem7  35428  satfv1  35579  dfon4  36107  onint1  36665  bj-2upln1upl  37272  poimirlem8  37879  dmcnvep  38639  dfssr2  38830  prjspval2  42971  diophren  43170  ordeldif1o  43617  nonrel  43940  dssmapntrcls  44484  salincl  46682  meaiuninc  46839  carageniuncllem1  46879  iscnrm3rlem3  49301