Theorem difeq2i 4098

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

Syntax hints:   = wceq 1537   ∖ cdif 3935

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 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149  df-dif 3941

This theorem is referenced by:  difeq12i  4099  dfun3  4244  dfin3  4245  dfin4  4246  invdif  4247  indif  4248  difundi  4258  difindi  4260  difdif2  4263  dif32  4269  difabs  4270  dfsymdif3  4271  notrab  4282  dif0  4334  unvdif  4425  difdifdir  4439  dfif3  4483  difpr  4738  iinvdif  5004  cnvin  6005  fndifnfp  6940  dif1o  8127  dfsdom2  8642  dju1dif  9600  m1bits  15791  clsval2  21660  mretopd  21702  cmpfi  22018  llycmpkgen2  22160  pserdvlem2  25018  nbgrssvwo2  27146  finsumvtxdg2ssteplem1  27329  frgrwopreglem3  28095  iundifdifd  30315  iundifdif  30316  difres  30352  pmtrcnelor  30737  cycpmconjv  30786  cyc3conja  30801  sibfof  31600  eulerpartlemmf  31635  kur14lem2  32456  kur14lem6  32460  kur14lem7  32461  satfv1  32612  dfon4  33356  onint1  33799  bj-2upln1upl  34338  poimirlem8  34902  dfssr2  35741  prjspval2  39270  diophren  39417  nonrel  39951  dssmapntrcls  40485  salincl  42615  meaiuninc  42770  carageniuncllem1  42810