Theorem difeq1i 4102

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

Syntax hints:   = wceq 1539   ∖ cdif 3928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-dif 3934

This theorem is referenced by:  difeq12i  4104  dfin3  4257  indif1  4262  indifcom  4263  difun1  4279  notab  4294  rabdif  4301  notrab  4302  undifabs  4458  difprsn1  4780  difprsn2  4781  diftpsn3  4782  resdifcom  5996  resdmdfsn  6029  frpoind  6342  wfiOLD  6351  orddif  6460  fresaun  6759  f12dfv  7275  f13dfv  7276  domunsncan  9094  phplem1OLD  9236  elfiun  9452  frind  9772  dju1dif  10195  axcclem  10479  dfn2  12522  mvdco  19431  pmtrdifellem2  19463  islinds2  21787  lindsind2  21793  restcld  23126  ufprim  23863  volun  25516  itgsplitioo  25809  uhgr0vb  29017  uhgr0  29018  uvtxupgrres  29353  cplgr3v  29380  ex-dif  30370  indifundif  32471  imadifxp  32549  aciunf1  32608  indsupp  32792  s1chn  32939  pmtrcnelor  33050  lindsunlem  33610  lindsun  33611  braew  34202  carsgclctunlem1  34278  carsggect  34279  coinflippvt  34446  ballotlemfval0  34457  signstfvcl  34547  satf0  35336  onint1  36409  bj-2upln1upl  36984  bj-disj2r  36988  lindsenlbs  37581  poimirlem13  37599  poimirlem14  37600  poimirlem18  37604  poimirlem21  37607  poimirlem30  37616  itg2addnclem  37637  asindmre  37669  sucdifsn  38199  disjresundif  38203  ressucdifsn  38205  kelac2  43040  fourierdlem102  46180  fourierdlem114  46192  pwsal  46287  issald  46305  sge0fodjrnlem  46388  hoiprodp1  46560  lincext2  48330  disjdifb  48687