Theorem difeq1i 4059

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

This proof depends on syntax axioms:   = wceq 1569   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 4047

This theorem is used by:  difeq12i  4061  dfin3  4222  indif1  4227  indifcom  4228  difun1  4244  notab  4259  rabdif  4266  notrab  4267  undifabs  4433  difprsn1  4762  difprsn2  4763  diftpsn3  4764  resdifcom  5988  resdmdfsn  6020  resdmdfsnOLD  6021  frpoind  6345  orddif  6461  fresaun  6753  f12dfv  7281  f13dfv  7282  domunsncan  9097  elfiun  9423  frind  9755  dju1dif  10252  axcclem  10536  dfn2  12620  nulchn  18794  s1chn  18795  chnccat  18801  ex-chn1  18812  ex-chn2  18813  mvdco  19660  pmtrdifellem2  19692  islinds2  22120  lindsind2  22126  lindsenlbs  22158  restcld  23491  ufprim  24229  volun  25867  itgsplitioo  26159  uhgr0vb  29651  uhgr0  29652  uvtxupgrres  29990  cplgr3v  30017  ex-dif  31025  indifundif  33163  imadifxp  33238  aciunf1  33300  indsupp  33477  pmtrcnelor  33695  lindsunlem  34299  lindsun  34300  braew  34918  carsgclctunlem1  34992  carsggect  34993  coinflippvt  35160  ballotlemfval0  35171  signstfvcl  35245  acwer1prc  35803  satf0  36180  onint1  37280  bj-2upln1upl  37980  bj-disj2r  37984  poimirlem13  38595  poimirlem14  38596  poimirlem18  38600  poimirlem21  38603  poimirlem30  38612  itg2addnclem  38633  asindmre  38665  disjresundif  39222  dmxrnuncnvepres  39368  dmxrncnvepres2  39409  sucdifsn  39462  ressucdifsn  39464  kelac2  44111  fourierdlem102  47262  fourierdlem114  47274  pwsal  47369  issald  47387  sge0fodjrnlem  47470  hoiprodp1  47642  lincext2  49611  disjdifb  49964