Theorem difeq2i 4078

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-dif 3909

This theorem is used by:  difeq12i  4079  dfun3  4229  dfin3  4230  dfin4  4231  invdif  4232  indif  4233  difundi  4243  difindi  4245  difdif2  4249  dif32  4255  difabs  4256  dfsymdif3  4259  notrab  4275  dif0  4334  unvdif  4436  difdifdir  4454  dfif3  4504  difpr  4773  iinvdif  5048  cnvin  6143  fndifnfp  7180  dif1o  8491  dfsdom2  9095  brttrcl2  9690  ttrcltr  9692  rnttrcl  9698  dju1dif  10172  m1bits  16520  clsval2  23257  mretopd  23299  cmpfi  23615  llycmpkgen2  23758  pserdvlem2  26642  nbgrssvwo2  29770  finsumvtxdg2ssteplem1  29953  frgrwopreglem3  30736  iundifdifd  32977  iundifdif  32978  difres  33016  gsumhashmul  33451  pmtrcnelor  33475  cycpmconjv  33526  cyc3conja  33541  elrgspnsubrunlem2  33632  evlextv  33996  sibfof  34795  eulerpartlemmf  34830  fineqvnttrclselem1  35591  kur14lem2  35736  kur14lem6  35740  kur14lem7  35741  satfv1  35892  dfon4  36420  onint1  37017  bj-2upln1upl  37717  poimirlem8  38336  dmcnvep  39095  dfssr2  39286  prjspval2  43403  diophren  43598  ordeldif1o  44045  nonrel  44368  dssmapntrcls  44912  salincl  47096  meaiuninc  47253  carageniuncllem1  47293  iscnrm3rlem3  49777