Theorem difeq2i 4089

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

Syntax hints:   = wceq 1540   ∖ cdif 3914

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-dif 3920

This theorem is referenced by:  difeq12i  4090  dfun3  4242  dfin3  4243  dfin4  4244  invdif  4245  indif  4246  difundi  4256  difindi  4258  difdif2  4262  dif32  4268  difabs  4269  dfsymdif3  4272  notrab  4288  dif0  4344  unvdif  4441  difdifdir  4458  dfif3  4506  difpr  4770  iinvdif  5047  cnvin  6120  fndifnfp  7153  dif1o  8467  dfsdom2  9070  brttrcl2  9674  ttrcltr  9676  rnttrcl  9682  dju1dif  10133  m1bits  16417  clsval2  22944  mretopd  22986  cmpfi  23302  llycmpkgen2  23444  pserdvlem2  26345  nbgrssvwo2  29296  finsumvtxdg2ssteplem1  29480  frgrwopreglem3  30250  iundifdifd  32497  iundifdif  32498  difres  32536  gsumhashmul  33008  pmtrcnelor  33055  cycpmconjv  33106  cyc3conja  33121  elrgspnsubrunlem2  33206  sibfof  34338  eulerpartlemmf  34373  kur14lem2  35201  kur14lem6  35205  kur14lem7  35206  satfv1  35357  dfon4  35888  onint1  36444  bj-2upln1upl  37019  poimirlem8  37629  dmcnvep  38368  dfssr2  38497  prjspval2  42608  diophren  42808  ordeldif1o  43256  nonrel  43580  dssmapntrcls  44124  salincl  46329  meaiuninc  46486  carageniuncllem1  46526  iscnrm3rlem3  48934