Theorem difeq1i 4097

Description: Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
difeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
difeq1i	⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)

Proof of Theorem difeq1i

Step	Hyp	Ref	Expression
1		difeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		difeq1 4094	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)

Syntax hints:   = wceq 1540   ∖ cdif 3923

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-dif 3929

This theorem is referenced by:  difeq12i  4099  dfin3  4252  indif1  4257  indifcom  4258  difun1  4274  notab  4289  rabdif  4296  notrab  4297  undifabs  4453  difprsn1  4776  difprsn2  4777  diftpsn3  4778  resdifcom  5985  resdmdfsn  6018  frpoind  6331  wfiOLD  6340  orddif  6449  fresaun  6748  f12dfv  7265  f13dfv  7266  domunsncan  9084  phplem1OLD  9226  elfiun  9440  frind  9762  dju1dif  10185  axcclem  10469  dfn2  12512  mvdco  19424  pmtrdifellem2  19456  islinds2  21771  lindsind2  21777  restcld  23108  ufprim  23845  volun  25496  itgsplitioo  25789  uhgr0vb  28997  uhgr0  28998  uvtxupgrres  29333  cplgr3v  29360  ex-dif  30350  indifundif  32451  imadifxp  32528  aciunf1  32587  indsupp  32790  s1chn  32936  pmtrcnelor  33048  lindsunlem  33610  lindsun  33611  braew  34219  carsgclctunlem1  34295  carsggect  34296  coinflippvt  34463  ballotlemfval0  34474  signstfvcl  34551  satf0  35340  onint1  36413  bj-2upln1upl  36988  bj-disj2r  36992  lindsenlbs  37585  poimirlem13  37603  poimirlem14  37604  poimirlem18  37608  poimirlem21  37611  poimirlem30  37620  itg2addnclem  37641  asindmre  37673  sucdifsn  38203  disjresundif  38207  ressucdifsn  38209  kelac2  43036  fourierdlem102  46185  fourierdlem114  46197  pwsal  46292  issald  46310  sge0fodjrnlem  46393  hoiprodp1  46565  lincext2  48379  disjdifb  48736