MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difeq1i Structured version   Visualization version   GIF version

Theorem difeq1i 4093
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
StepHypRef Expression
1 difeq1i.1 . 2 𝐴 = 𝐵
2 difeq1 4090 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  cdif 3931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-rab 3145  df-dif 3937
This theorem is referenced by:  difeq12i  4095  dfin3  4241  indif1  4246  indifcom  4247  difun1  4262  notab  4271  notrab  4278  undifabs  4424  difprsn1  4725  difprsn2  4726  diftpsn3  4727  resdifcom  5865  resdmdfsn  5894  wfi  6174  orddif  6277  fresaun  6542  f12dfv  7022  f13dfv  7023  domunsncan  8609  phplem1  8688  elfiun  8886  dju1dif  9590  axcclem  9871  dfn2  11902  mvdco  18565  pmtrdifellem2  18597  islinds2  20949  lindsind2  20955  restcld  21772  ufprim  22509  volun  24138  itgsplitioo  24430  uhgr0vb  26849  uhgr0  26850  uvtxupgrres  27182  cplgr3v  27209  ex-dif  28194  indifundif  30277  imadifxp  30343  aciunf1  30400  pmtrcnelor  30728  lindsunlem  31008  lindsun  31009  braew  31489  carsgclctunlem1  31563  carsggect  31564  coinflippvt  31730  ballotlemfval0  31741  signstfvcl  31831  satf0  32607  frpoind  33068  frind  33073  onint1  33785  bj-2upln1upl  34324  bj-disj2r  34328  lindsenlbs  34874  poimirlem13  34892  poimirlem14  34893  poimirlem18  34897  poimirlem21  34900  poimirlem30  34909  itg2addnclem  34930  asindmre  34964  rabdif  39092  kelac2  39650  fourierdlem102  42478  fourierdlem114  42490  pwsal  42585  issald  42601  sge0fodjrnlem  42683  hoiprodp1  42855  lincext2  44495
  Copyright terms: Public domain W3C validator