Theorem difeq1i 3951

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

Syntax hints:   = wceq 1658   ∖ cdif 3795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-dif 3801

This theorem is referenced by:  difeq12i  3953  dfin3  4096  indif1  4101  indifcom  4102  difun1  4117  notab  4126  notrab  4133  undifabs  4268  difprsn1  4549  difprsn2  4550  diftpsn3  4551  resdifcom  5652  resdmdfsn  5682  wfi  5953  orddif  6056  fresaun  6312  f12dfv  6784  f13dfv  6785  domunsncan  8329  phplem1  8408  elfiun  8605  axcclem  9594  dfn2  11633  mvdco  18215  pmtrdifellem2  18247  islinds2  20519  lindsind2  20525  restcld  21347  ufprim  22083  volun  23711  itgsplitioo  24003  uhgr0vb  26370  uhgr0  26371  uvtxupgrres  26706  cplgr3v  26733  ex-dif  27838  indifundif  29904  imadifxp  29961  aciunf1  30012  braew  30850  carsgclctunlem1  30924  carsggect  30925  coinflippvt  31092  ballotlemfval0  31103  signstfvcl  31198  frpoind  32279  frind  32282  onint1  32981  bj-2upln1upl  33534  bj-disj2r  33535  lindsenlbs  33948  poimirlem13  33966  poimirlem14  33967  poimirlem18  33971  poimirlem21  33974  poimirlem30  33983  itg2addnclem  34004  asindmre  34038  kelac2  38478  fourierdlem102  41219  fourierdlem114  41231  pwsal  41326  issald  41342  sge0fodjrnlem  41424  hoiprodp1  41596  lincext2  43091