Theorem difeq1i 4053

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

Syntax hints:   = wceq 1539   ∖ cdif 3884

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-dif 3890

This theorem is referenced by:  difeq12i  4055  dfin3  4200  indif1  4205  indifcom  4206  difun1  4223  notab  4238  notrab  4245  undifabs  4411  difprsn1  4733  difprsn2  4734  diftpsn3  4735  resdifcom  5910  resdmdfsn  5941  frpoind  6245  wfiOLD  6254  orddif  6359  fresaun  6645  f12dfv  7145  f13dfv  7146  domunsncan  8859  phplem1OLD  9000  elfiun  9189  frind  9508  dju1dif  9928  axcclem  10213  dfn2  12246  mvdco  19053  pmtrdifellem2  19085  islinds2  21020  lindsind2  21026  restcld  22323  ufprim  23060  volun  24709  itgsplitioo  25002  uhgr0vb  27442  uhgr0  27443  uvtxupgrres  27775  cplgr3v  27802  ex-dif  28787  indifundif  30873  imadifxp  30940  aciunf1  31000  pmtrcnelor  31360  lindsunlem  31705  lindsun  31706  braew  32210  carsgclctunlem1  32284  carsggect  32285  coinflippvt  32451  ballotlemfval0  32462  signstfvcl  32552  satf0  33334  onint1  34638  bj-2upln1upl  35214  bj-disj2r  35218  lindsenlbs  35772  poimirlem13  35790  poimirlem14  35791  poimirlem18  35795  poimirlem21  35798  poimirlem30  35807  itg2addnclem  35828  asindmre  35860  rabdif  40184  kelac2  40890  fourierdlem102  43749  fourierdlem114  43761  pwsal  43856  issald  43872  sge0fodjrnlem  43954  hoiprodp1  44126  lincext2  45796  disjdifb  46155