Theorem difeq1i 4119

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

Syntax hints:   = wceq 1542   ∖ cdif 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-dif 3952

This theorem is referenced by:  difeq12i  4121  dfin3  4267  indif1  4272  indifcom  4273  difun1  4290  notab  4305  notrab  4312  undifabs  4478  difprsn1  4804  difprsn2  4805  diftpsn3  4806  resdifcom  6001  resdmdfsn  6032  frpoind  6344  wfiOLD  6353  orddif  6461  fresaun  6763  f12dfv  7271  f13dfv  7272  domunsncan  9072  phplem1OLD  9217  elfiun  9425  frind  9745  dju1dif  10167  axcclem  10452  dfn2  12485  mvdco  19313  pmtrdifellem2  19345  islinds2  21368  lindsind2  21374  restcld  22676  ufprim  23413  volun  25062  itgsplitioo  25355  uhgr0vb  28363  uhgr0  28364  uvtxupgrres  28696  cplgr3v  28723  ex-dif  29707  indifundif  31793  imadifxp  31863  aciunf1  31919  pmtrcnelor  32283  lindsunlem  32740  lindsun  32741  braew  33271  carsgclctunlem1  33347  carsggect  33348  coinflippvt  33514  ballotlemfval0  33525  signstfvcl  33615  satf0  34394  onint1  35382  bj-2upln1upl  35953  bj-disj2r  35957  lindsenlbs  36531  poimirlem13  36549  poimirlem14  36550  poimirlem18  36554  poimirlem21  36557  poimirlem30  36566  itg2addnclem  36587  asindmre  36619  sucdifsn  37153  disjresundif  37157  ressucdifsn  37159  rabdif  41080  kelac2  41855  fourierdlem102  44972  fourierdlem114  44984  pwsal  45079  issald  45097  sge0fodjrnlem  45180  hoiprodp1  45352  lincext2  47184  disjdifb  47542