Theorem difeq2i 4096

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

Syntax hints:   = wceq 1537   ∖ cdif 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-dif 3939

This theorem is referenced by:  difeq12i  4097  dfun3  4242  dfin3  4243  dfin4  4244  invdif  4245  indif  4246  difundi  4256  difindi  4258  difdif2  4261  dif32  4267  difabs  4268  dfsymdif3  4269  notrab  4280  dif0  4332  unvdif  4423  difdifdir  4437  dfif3  4481  difpr  4736  iinvdif  5002  cnvin  6003  fndifnfp  6938  dif1o  8125  dfsdom2  8640  dju1dif  9598  m1bits  15789  clsval2  21658  mretopd  21700  cmpfi  22016  llycmpkgen2  22158  pserdvlem2  25016  nbgrssvwo2  27144  finsumvtxdg2ssteplem1  27327  frgrwopreglem3  28093  iundifdifd  30313  iundifdif  30314  difres  30350  pmtrcnelor  30735  cycpmconjv  30784  cyc3conja  30799  sibfof  31598  eulerpartlemmf  31633  kur14lem2  32454  kur14lem6  32458  kur14lem7  32459  satfv1  32610  dfon4  33354  onint1  33797  bj-2upln1upl  34339  poimirlem8  34915  dfssr2  35754  prjspval2  39283  diophren  39430  nonrel  39964  dssmapntrcls  40498  salincl  42628  meaiuninc  42783  carageniuncllem1  42823