Theorem difeq1i 4063

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

Syntax hints:   = wceq 1542   ∖ cdif 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-dif 3893

This theorem is referenced by:  difeq12i  4065  dfin3  4218  indif1  4223  indifcom  4224  difun1  4240  notab  4255  rabdif  4262  notrab  4263  undifabs  4419  difprsn1  4744  difprsn2  4745  diftpsn3  4746  resdifcom  5957  resdmdfsn  5990  frpoind  6300  orddif  6415  fresaun  6705  f12dfv  7221  f13dfv  7222  domunsncan  9008  elfiun  9336  frind  9665  dju1dif  10086  axcclem  10370  dfn2  12441  nulchn  18576  s1chn  18577  chnccat  18583  ex-chn1  18594  ex-chn2  18595  mvdco  19411  pmtrdifellem2  19443  islinds2  21803  lindsind2  21809  restcld  23147  ufprim  23884  volun  25522  itgsplitioo  25815  uhgr0vb  29155  uhgr0  29156  uvtxupgrres  29491  cplgr3v  29518  ex-dif  30508  indifundif  32609  imadifxp  32686  aciunf1  32751  indsupp  32942  pmtrcnelor  33167  lindsunlem  33784  lindsun  33785  braew  34402  carsgclctunlem1  34477  carsggect  34478  coinflippvt  34645  ballotlemfval0  34656  signstfvcl  34733  satf0  35570  onint1  36647  bj-2upln1upl  37347  bj-disj2r  37351  lindsenlbs  37950  poimirlem13  37968  poimirlem14  37969  poimirlem18  37973  poimirlem21  37976  poimirlem30  37985  itg2addnclem  38006  asindmre  38038  disjresundif  38581  dmxrnuncnvepres  38727  dmxrncnvepres2  38768  sucdifsn  38821  ressucdifsn  38823  kelac2  43511  fourierdlem102  46654  fourierdlem114  46666  pwsal  46761  issald  46779  sge0fodjrnlem  46862  hoiprodp1  47034  lincext2  48943  disjdifb  49297