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  28332  uhgr0  28333  uvtxupgrres  28665  cplgr3v  28692  ex-dif  29676  indifundif  31762  imadifxp  31832  aciunf1  31888  pmtrcnelor  32252  lindsunlem  32709  lindsun  32710  braew  33240  carsgclctunlem1  33316  carsggect  33317  coinflippvt  33483  ballotlemfval0  33494  signstfvcl  33584  satf0  34363  onint1  35334  bj-2upln1upl  35905  bj-disj2r  35909  lindsenlbs  36483  poimirlem13  36501  poimirlem14  36502  poimirlem18  36506  poimirlem21  36509  poimirlem30  36518  itg2addnclem  36539  asindmre  36571  sucdifsn  37105  disjresundif  37109  ressucdifsn  37111  rabdif  41032  kelac2  41807  fourierdlem102  44924  fourierdlem114  44936  pwsal  45031  issald  45049  sge0fodjrnlem  45132  hoiprodp1  45304  lincext2  47136  disjdifb  47494