Theorem difeq1i 4070

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3902

This theorem is used by:  difeq12i  4072  dfin3  4223  indif1  4228  indifcom  4229  difun1  4245  notab  4260  rabdif  4267  notrab  4268  undifabs  4434  difprsn1  4763  difprsn2  4764  diftpsn3  4765  resdifcom  5989  resdmdfsn  6021  resdmdfsnOLD  6022  frpoind  6344  orddif  6460  fresaun  6751  f12dfv  7279  f13dfv  7280  domunsncan  9089  elfiun  9415  frind  9747  dju1dif  10244  axcclem  10528  dfn2  12612  nulchn  18786  s1chn  18787  chnccat  18793  ex-chn1  18804  ex-chn2  18805  mvdco  19652  pmtrdifellem2  19684  islinds2  22112  lindsind2  22118  lindsenlbs  22150  restcld  23483  ufprim  24221  volun  25859  itgsplitioo  26151  uhgr0vb  29643  uhgr0  29644  uvtxupgrres  29982  cplgr3v  30009  ex-dif  31017  indifundif  33113  imadifxp  33188  aciunf1  33250  indsupp  33427  pmtrcnelor  33645  lindsunlem  34249  lindsun  34250  braew  34868  carsgclctunlem1  34942  carsggect  34943  coinflippvt  35110  ballotlemfval0  35121  signstfvcl  35195  satf0  36116  onint1  37217  bj-2upln1upl  37917  bj-disj2r  37921  poimirlem13  38531  poimirlem14  38532  poimirlem18  38536  poimirlem21  38539  poimirlem30  38548  itg2addnclem  38569  asindmre  38601  disjresundif  39158  dmxrnuncnvepres  39304  dmxrncnvepres2  39345  sucdifsn  39398  ressucdifsn  39400  kelac2  44051  fourierdlem102  47187  fourierdlem114  47199  pwsal  47294  issald  47312  sge0fodjrnlem  47395  hoiprodp1  47567  lincext2  49536  disjdifb  49889