Theorem difeq1i 4085

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

Syntax hints:   = wceq 1567   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-dif 3916

This theorem is referenced by:  difeq12i  4087  dfin3  4238  indif1  4243  indifcom  4244  difun1  4260  notab  4275  rabdif  4282  notrab  4283  undifabs  4441  difprsn1  4769  difprsn2  4770  diftpsn3  4771  resdifcom  5995  resdmdfsn  6029  resdmdfsnOLD  6030  frpoind  6341  orddif  6457  fresaun  6747  f12dfv  7269  f13dfv  7270  domunsncan  9061  elfiun  9386  frind  9718  dju1dif  10152  axcclem  10437  dfn2  12513  nulchn  18671  s1chn  18672  chnccat  18678  ex-chn1  18689  ex-chn2  18690  mvdco  19511  pmtrdifellem2  19543  islinds2  21928  lindsind2  21934  restcld  23294  ufprim  24031  volun  25669  itgsplitioo  25962  uhgr0vb  29359  uhgr0  29360  uvtxupgrres  29695  cplgr3v  29722  ex-dif  30711  indifundif  32807  imadifxp  32883  aciunf1  32945  indsupp  33124  pmtrcnelor  33348  lindsunlem  33955  lindsun  33956  braew  34573  carsgclctunlem1  34648  carsggect  34649  coinflippvt  34816  ballotlemfval0  34827  signstfvcl  34901  satf0  35759  onint1  36845  bj-2upln1upl  37544  bj-disj2r  37548  lindsenlbs  38149  poimirlem13  38167  poimirlem14  38168  poimirlem18  38172  poimirlem21  38175  poimirlem30  38184  itg2addnclem  38205  asindmre  38237  disjresundif  38780  dmxrnuncnvepres  38926  dmxrncnvepres2  38967  sucdifsn  39020  ressucdifsn  39022  kelac2  43679  fourierdlem102  46809  fourierdlem114  46821  pwsal  46916  issald  46934  sge0fodjrnlem  47017  hoiprodp1  47189  lincext2  49115  disjdifb  49468