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 1547   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-dif 3886

This theorem is referenced by:  difeq12i  4055  dfin3  4205  indif1  4210  indifcom  4211  difun1  4227  notab  4242  rabdif  4249  notrab  4250  undifabs  4406  difprsn1  4733  difprsn2  4734  diftpsn3  4735  resdifcom  5950  resdmdfsn  5983  frpoind  6293  orddif  6408  fresaun  6698  f12dfv  7217  f13dfv  7218  domunsncan  9005  elfiun  9333  frind  9665  dju1dif  10086  axcclem  10370  dfn2  12441  nulchn  18576  s1chn  18577  chnccat  18583  ex-chn1  18594  ex-chn2  18595  mvdco  19411  pmtrdifellem2  19443  islinds2  21788  lindsind2  21794  restcld  23155  ufprim  23892  volun  25530  itgsplitioo  25823  uhgr0vb  29159  uhgr0  29160  uvtxupgrres  29495  cplgr3v  29522  ex-dif  30511  indifundif  32612  imadifxp  32690  aciunf1  32755  indsupp  32946  pmtrcnelor  33172  lindsunlem  33808  lindsun  33809  braew  34426  carsgclctunlem1  34501  carsggect  34502  coinflippvt  34669  ballotlemfval0  34680  signstfvcl  34757  satf0  35600  onint1  36677  bj-2upln1upl  37377  bj-disj2r  37381  lindsenlbs  37982  poimirlem13  38000  poimirlem14  38001  poimirlem18  38005  poimirlem21  38008  poimirlem30  38017  itg2addnclem  38038  asindmre  38070  disjresundif  38613  dmxrnuncnvepres  38759  dmxrncnvepres2  38800  sucdifsn  38853  ressucdifsn  38855  kelac2  43510  fourierdlem102  46651  fourierdlem114  46663  pwsal  46758  issald  46776  sge0fodjrnlem  46859  hoiprodp1  47031  lincext2  48946  disjdifb  49300