Theorem difeq2i 4132

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

Syntax hints:   = wceq 1536   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-dif 3965

This theorem is referenced by:  difeq12i  4133  dfun3  4281  dfin3  4282  dfin4  4283  invdif  4284  indif  4285  difundi  4295  difindi  4297  difdif2  4301  dif32  4307  difabs  4308  dfsymdif3  4311  notrab  4327  dif0  4383  unvdif  4480  difdifdir  4497  dfif3  4544  difpr  4807  iinvdif  5084  cnvin  6166  fndifnfp  7195  dif1o  8536  dfsdom2  9134  brttrcl2  9751  ttrcltr  9753  rnttrcl  9759  dju1dif  10210  m1bits  16473  clsval2  23073  mretopd  23115  cmpfi  23431  llycmpkgen2  23573  pserdvlem2  26486  nbgrssvwo2  29393  finsumvtxdg2ssteplem1  29577  frgrwopreglem3  30342  iundifdifd  32581  iundifdif  32582  difres  32619  gsumhashmul  33046  pmtrcnelor  33093  cycpmconjv  33144  cyc3conja  33159  sibfof  34321  eulerpartlemmf  34356  kur14lem2  35191  kur14lem6  35195  kur14lem7  35196  satfv1  35347  dfon4  35874  onint1  36431  bj-2upln1upl  37006  poimirlem8  37614  dfssr2  38480  prjspval2  42599  diophren  42800  ordeldif1o  43249  nonrel  43573  dssmapntrcls  44117  salincl  46279  meaiuninc  46436  carageniuncllem1  46476  iscnrm3rlem3  48738