Theorem difeq2i 4120

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

Syntax hints:   = wceq 1542   ∖ cdif 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-dif 3952

This theorem is referenced by:  difeq12i  4121  dfun3  4266  dfin3  4267  dfin4  4268  invdif  4269  indif  4270  difundi  4280  difindi  4282  difdif2  4287  dif32  4293  difabs  4294  dfsymdif3  4297  notrab  4312  dif0  4373  unvdif  4475  difdifdir  4492  dfif3  4543  difpr  4807  iinvdif  5084  cnvin  6145  fndifnfp  7174  dif1o  8500  dfsdom2  9096  brttrcl2  9709  ttrcltr  9711  rnttrcl  9717  dju1dif  10167  m1bits  16381  clsval2  22554  mretopd  22596  cmpfi  22912  llycmpkgen2  23054  pserdvlem2  25940  nbgrssvwo2  28650  finsumvtxdg2ssteplem1  28833  frgrwopreglem3  29598  iundifdifd  31824  iundifdif  31825  difres  31862  gsumhashmul  32239  pmtrcnelor  32283  cycpmconjv  32332  cyc3conja  32347  sibfof  33370  eulerpartlemmf  33405  kur14lem2  34229  kur14lem6  34233  kur14lem7  34234  satfv1  34385  dfon4  34896  onint1  35382  bj-2upln1upl  35953  poimirlem8  36544  dfssr2  37417  prjspval2  41403  diophren  41599  ordeldif1o  42058  nonrel  42383  dssmapntrcls  42927  salincl  45088  meaiuninc  45245  carageniuncllem1  45285  iscnrm3rlem3  47623