Theorem difeq1i 4071

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

Syntax hints:   = wceq 1541   ∖ cdif 3895

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-dif 3901

This theorem is referenced by:  difeq12i  4073  dfin3  4226  indif1  4231  indifcom  4232  difun1  4248  notab  4263  rabdif  4270  notrab  4271  undifabs  4427  difprsn1  4753  difprsn2  4754  diftpsn3  4755  resdifcom  5954  resdmdfsn  5987  frpoind  6297  orddif  6412  fresaun  6702  f12dfv  7216  f13dfv  7217  domunsncan  9001  elfiun  9325  frind  9654  dju1dif  10075  axcclem  10359  dfn2  12405  nulchn  18533  s1chn  18534  chnccat  18540  ex-chn1  18551  ex-chn2  18552  mvdco  19365  pmtrdifellem2  19397  islinds2  21759  lindsind2  21765  restcld  23107  ufprim  23844  volun  25493  itgsplitioo  25786  uhgr0vb  29071  uhgr0  29072  uvtxupgrres  29407  cplgr3v  29434  ex-dif  30424  indifundif  32525  imadifxp  32602  aciunf1  32667  indsupp  32877  pmtrcnelor  33101  lindsunlem  33709  lindsun  33710  braew  34327  carsgclctunlem1  34402  carsggect  34403  coinflippvt  34570  ballotlemfval0  34581  signstfvcl  34658  satf0  35488  onint1  36565  bj-2upln1upl  37141  bj-disj2r  37145  lindsenlbs  37728  poimirlem13  37746  poimirlem14  37747  poimirlem18  37751  poimirlem21  37754  poimirlem30  37763  itg2addnclem  37784  asindmre  37816  disjresundif  38354  dmxrnuncnvepres  38489  dmxrncnvepres2  38530  sucdifsn  38571  ressucdifsn  38573  kelac2  43222  fourierdlem102  46368  fourierdlem114  46380  pwsal  46475  issald  46493  sge0fodjrnlem  46576  hoiprodp1  46748  lincext2  48617  disjdifb  48971