Theorem difeq2i 4082

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

Syntax hints:   = wceq 1540   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-dif 3914

This theorem is referenced by:  difeq12i  4083  dfun3  4235  dfin3  4236  dfin4  4237  invdif  4238  indif  4239  difundi  4249  difindi  4251  difdif2  4255  dif32  4261  difabs  4262  dfsymdif3  4265  notrab  4281  dif0  4337  unvdif  4434  difdifdir  4451  dfif3  4499  difpr  4763  iinvdif  5039  cnvin  6105  fndifnfp  7132  dif1o  8441  dfsdom2  9041  brttrcl2  9643  ttrcltr  9645  rnttrcl  9651  dju1dif  10102  m1bits  16386  clsval2  22913  mretopd  22955  cmpfi  23271  llycmpkgen2  23413  pserdvlem2  26314  nbgrssvwo2  29265  finsumvtxdg2ssteplem1  29449  frgrwopreglem3  30216  iundifdifd  32463  iundifdif  32464  difres  32502  gsumhashmul  32974  pmtrcnelor  33021  cycpmconjv  33072  cyc3conja  33087  elrgspnsubrunlem2  33172  sibfof  34304  eulerpartlemmf  34339  kur14lem2  35167  kur14lem6  35171  kur14lem7  35172  satfv1  35323  dfon4  35854  onint1  36410  bj-2upln1upl  36985  poimirlem8  37595  dmcnvep  38334  dfssr2  38463  prjspval2  42574  diophren  42774  ordeldif1o  43222  nonrel  43546  dssmapntrcls  44090  salincl  46295  meaiuninc  46452  carageniuncllem1  46492  iscnrm3rlem3  48903