Theorem difeq2i 4119

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

Syntax hints:   = wceq 1541   ∖ cdif 3945

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-dif 3951

This theorem is referenced by:  difeq12i  4120  dfun3  4265  dfin3  4266  dfin4  4267  invdif  4268  indif  4269  difundi  4279  difindi  4281  difdif2  4286  dif32  4292  difabs  4293  dfsymdif3  4296  notrab  4311  dif0  4372  unvdif  4474  difdifdir  4491  dfif3  4542  difpr  4806  iinvdif  5083  cnvin  6144  fndifnfp  7173  dif1o  8499  dfsdom2  9095  brttrcl2  9708  ttrcltr  9710  rnttrcl  9716  dju1dif  10166  m1bits  16380  clsval2  22553  mretopd  22595  cmpfi  22911  llycmpkgen2  23053  pserdvlem2  25939  nbgrssvwo2  28616  finsumvtxdg2ssteplem1  28799  frgrwopreglem3  29564  iundifdifd  31788  iundifdif  31789  difres  31826  gsumhashmul  32203  pmtrcnelor  32247  cycpmconjv  32296  cyc3conja  32311  sibfof  33334  eulerpartlemmf  33369  kur14lem2  34193  kur14lem6  34197  kur14lem7  34198  satfv1  34349  dfon4  34860  onint1  35329  bj-2upln1upl  35900  poimirlem8  36491  dfssr2  37364  prjspval2  41356  diophren  41541  ordeldif1o  42000  nonrel  42325  dssmapntrcls  42869  salincl  45030  meaiuninc  45187  carageniuncllem1  45227  iscnrm3rlem3  47565