Theorem difeq1i 4049

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

Syntax hints:   = wceq 1539   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-dif 3886

This theorem is referenced by:  difeq12i  4051  dfin3  4197  indif1  4202  indifcom  4203  difun1  4220  notab  4235  notrab  4242  undifabs  4408  difprsn1  4730  difprsn2  4731  diftpsn3  4732  resdifcom  5899  resdmdfsn  5930  frpoind  6230  wfiOLD  6239  orddif  6344  fresaun  6629  f12dfv  7126  f13dfv  7127  domunsncan  8812  phplem1  8892  elfiun  9119  frind  9439  dju1dif  9859  axcclem  10144  dfn2  12176  mvdco  18968  pmtrdifellem2  19000  islinds2  20930  lindsind2  20936  restcld  22231  ufprim  22968  volun  24614  itgsplitioo  24907  uhgr0vb  27345  uhgr0  27346  uvtxupgrres  27678  cplgr3v  27705  ex-dif  28688  indifundif  30774  imadifxp  30841  aciunf1  30902  pmtrcnelor  31262  lindsunlem  31607  lindsun  31608  braew  32110  carsgclctunlem1  32184  carsggect  32185  coinflippvt  32351  ballotlemfval0  32362  signstfvcl  32452  satf0  33234  onint1  34565  bj-2upln1upl  35141  bj-disj2r  35145  lindsenlbs  35699  poimirlem13  35717  poimirlem14  35718  poimirlem18  35722  poimirlem21  35725  poimirlem30  35734  itg2addnclem  35755  asindmre  35787  rabdif  40112  kelac2  40806  fourierdlem102  43639  fourierdlem114  43651  pwsal  43746  issald  43762  sge0fodjrnlem  43844  hoiprodp1  44016  lincext2  45684  disjdifb  46043