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 1541   ∖ cdif 3902

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 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-dif 3908

This theorem is referenced by:  difeq12i  4075  dfun3  4220  dfin3  4221  dfin4  4222  invdif  4223  indif  4224  difundi  4234  difindi  4236  difdif2  4241  dif32  4247  difabs  4248  dfsymdif3  4251  notrab  4266  dif0  4327  unvdif  4429  difdifdir  4444  dfif3  4495  difpr  4758  iinvdif  5035  cnvin  6090  fndifnfp  7113  dif1o  8410  dfsdom2  8970  brttrcl2  9580  ttrcltr  9582  rnttrcl  9588  dju1dif  10038  m1bits  16251  clsval2  22311  mretopd  22353  cmpfi  22669  llycmpkgen2  22811  pserdvlem2  25697  nbgrssvwo2  28084  finsumvtxdg2ssteplem1  28267  frgrwopreglem3  29032  iundifdifd  31252  iundifdif  31253  difres  31290  gsumhashmul  31667  pmtrcnelor  31711  cycpmconjv  31760  cyc3conja  31775  sibfof  32671  eulerpartlemmf  32706  kur14lem2  33532  kur14lem6  33536  kur14lem7  33537  satfv1  33688  dfon4  34334  onint1  34777  bj-2upln1upl  35351  poimirlem8  35941  dfssr2  36817  prjspval2  40763  diophren  40948  nonrel  41565  dssmapntrcls  42111  salincl  44252  meaiuninc  44408  carageniuncllem1  44448  iscnrm3rlem3  46653