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

Theorem difeq1i 3707
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 3704 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  cdif 3556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-dif 3562
This theorem is referenced by:  difeq12i  3709  dfin3  3847  indif1  3852  indifcom  3853  difun1  3868  notab  3878  notrab  3885  undifabs  4022  difprsn1  4304  difprsn2  4305  diftpsn3  4306  resdifcom  5379  resdmdfsn  5409  wfi  5677  orddif  5784  fresaun  6037  f12dfv  6489  f13dfv  6490  domunsncan  8012  phplem1  8091  elfiun  8288  axcclem  9231  dfn2  11257  mvdco  17797  pmtrdifellem2  17829  islinds2  20084  lindsind2  20090  restcld  20899  ufprim  21636  volun  23236  itgsplitioo  23527  uhgr0vb  25880  uhgr0  25881  uvtxupgrres  26213  cplgr3v  26235  konigsbergiedgwOLD  26992  ex-dif  27151  indifundif  29226  imadifxp  29282  aciunf1  29328  braew  30110  carsgclctunlem1  30184  carsggect  30185  coinflippvt  30351  ballotlemfval0  30362  signstfvcl  30454  frind  31476  onint1  32125  bj-2upln1upl  32694  bj-disj2r  32695  lindsenlbs  33071  poimirlem13  33089  poimirlem14  33090  poimirlem18  33094  poimirlem21  33097  poimirlem30  33106  itg2addnclem  33128  asindmre  33162  kelac2  37150  fourierdlem102  39758  fourierdlem114  39770  pwsal  39868  issald  39884  sge0fodjrnlem  39966  hoiprodp1  40135  lincext2  41558
  Copyright terms: Public domain W3C validator