Theorem difeq1i 4062

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

Syntax hints:   = wceq 1542   ∖ cdif 3886

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-dif 3892

This theorem is referenced by:  difeq12i  4064  dfin3  4217  indif1  4222  indifcom  4223  difun1  4239  notab  4254  rabdif  4261  notrab  4262  undifabs  4418  difprsn1  4745  difprsn2  4746  diftpsn3  4747  resdifcom  5963  resdmdfsn  5996  frpoind  6306  orddif  6421  fresaun  6711  f12dfv  7228  f13dfv  7229  domunsncan  9015  elfiun  9343  frind  9674  dju1dif  10095  axcclem  10379  dfn2  12450  nulchn  18585  s1chn  18586  chnccat  18592  ex-chn1  18603  ex-chn2  18604  mvdco  19420  pmtrdifellem2  19452  islinds2  21793  lindsind2  21799  restcld  23137  ufprim  23874  volun  25512  itgsplitioo  25805  uhgr0vb  29141  uhgr0  29142  uvtxupgrres  29477  cplgr3v  29504  ex-dif  30493  indifundif  32594  imadifxp  32671  aciunf1  32736  indsupp  32927  pmtrcnelor  33152  lindsunlem  33768  lindsun  33769  braew  34386  carsgclctunlem1  34461  carsggect  34462  coinflippvt  34629  ballotlemfval0  34640  signstfvcl  34717  satf0  35554  onint1  36631  bj-2upln1upl  37331  bj-disj2r  37335  lindsenlbs  37936  poimirlem13  37954  poimirlem14  37955  poimirlem18  37959  poimirlem21  37962  poimirlem30  37971  itg2addnclem  37992  asindmre  38024  disjresundif  38567  dmxrnuncnvepres  38713  dmxrncnvepres2  38754  sucdifsn  38807  ressucdifsn  38809  kelac2  43493  fourierdlem102  46636  fourierdlem114  46648  pwsal  46743  issald  46761  sge0fodjrnlem  46844  hoiprodp1  47016  lincext2  48931  disjdifb  49285