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  22970  mretopd  23012  cmpfi  23328  llycmpkgen2  23470  pserdvlem2  26371  nbgrssvwo2  29342  finsumvtxdg2ssteplem1  29526  frgrwopreglem3  30293  iundifdifd  32540  iundifdif  32541  difres  32579  gsumhashmul  33044  pmtrcnelor  33063  cycpmconjv  33114  cyc3conja  33129  elrgspnsubrunlem2  33215  sibfof  34324  eulerpartlemmf  34359  kur14lem2  35187  kur14lem6  35191  kur14lem7  35192  satfv1  35343  dfon4  35874  onint1  36430  bj-2upln1upl  37005  poimirlem8  37615  dmcnvep  38354  dfssr2  38483  prjspval2  42594  diophren  42794  ordeldif1o  43242  nonrel  43566  dssmapntrcls  44110  salincl  46315  meaiuninc  46472  carageniuncllem1  46512  iscnrm3rlem3  48923