Theorem difeq1i 4074

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

Syntax hints:   = wceq 1541   ∖ cdif 3898

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-dif 3904

This theorem is referenced by:  difeq12i  4076  dfin3  4229  indif1  4234  indifcom  4235  difun1  4251  notab  4266  rabdif  4273  notrab  4274  undifabs  4430  difprsn1  4756  difprsn2  4757  diftpsn3  4758  resdifcom  5957  resdmdfsn  5990  frpoind  6300  orddif  6415  fresaun  6705  f12dfv  7219  f13dfv  7220  domunsncan  9005  elfiun  9333  frind  9662  dju1dif  10083  axcclem  10367  dfn2  12414  nulchn  18542  s1chn  18543  chnccat  18549  ex-chn1  18560  ex-chn2  18561  mvdco  19374  pmtrdifellem2  19406  islinds2  21768  lindsind2  21774  restcld  23116  ufprim  23853  volun  25502  itgsplitioo  25795  uhgr0vb  29145  uhgr0  29146  uvtxupgrres  29481  cplgr3v  29508  ex-dif  30498  indifundif  32599  imadifxp  32676  aciunf1  32741  indsupp  32949  pmtrcnelor  33173  lindsunlem  33781  lindsun  33782  braew  34399  carsgclctunlem1  34474  carsggect  34475  coinflippvt  34642  ballotlemfval0  34653  signstfvcl  34730  satf0  35566  onint1  36643  bj-2upln1upl  37225  bj-disj2r  37229  lindsenlbs  37816  poimirlem13  37834  poimirlem14  37835  poimirlem18  37839  poimirlem21  37842  poimirlem30  37851  itg2addnclem  37872  asindmre  37904  disjresundif  38442  dmxrnuncnvepres  38577  dmxrncnvepres2  38618  sucdifsn  38659  ressucdifsn  38661  kelac2  43307  fourierdlem102  46452  fourierdlem114  46464  pwsal  46559  issald  46577  sge0fodjrnlem  46660  hoiprodp1  46832  lincext2  48701  disjdifb  49055