Theorem difeq2i 4074

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

Syntax hints:   = wceq 1540   ∖ cdif 3900

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

This theorem is referenced by:  difeq12i  4075  dfun3  4227  dfin3  4228  dfin4  4229  invdif  4230  indif  4231  difundi  4241  difindi  4243  difdif2  4247  dif32  4253  difabs  4254  dfsymdif3  4257  notrab  4273  dif0  4329  unvdif  4426  difdifdir  4443  dfif3  4491  difpr  4754  iinvdif  5029  cnvin  6093  fndifnfp  7112  dif1o  8418  dfsdom2  9017  brttrcl2  9610  ttrcltr  9612  rnttrcl  9618  dju1dif  10067  m1bits  16351  clsval2  22935  mretopd  22977  cmpfi  23293  llycmpkgen2  23435  pserdvlem2  26336  nbgrssvwo2  29307  finsumvtxdg2ssteplem1  29491  frgrwopreglem3  30258  iundifdifd  32505  iundifdif  32506  difres  32544  gsumhashmul  33014  pmtrcnelor  33033  cycpmconjv  33084  cyc3conja  33099  elrgspnsubrunlem2  33188  sibfof  34308  eulerpartlemmf  34343  kur14lem2  35180  kur14lem6  35184  kur14lem7  35185  satfv1  35336  dfon4  35867  onint1  36423  bj-2upln1upl  36998  poimirlem8  37608  dmcnvep  38347  dfssr2  38476  prjspval2  42586  diophren  42786  ordeldif1o  43233  nonrel  43557  dssmapntrcls  44101  salincl  46305  meaiuninc  46462  carageniuncllem1  46502  iscnrm3rlem3  48926