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

Theorem difeq2i 4082
Description: Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
difeq2i (𝐶𝐴) = (𝐶𝐵)

Proof of Theorem difeq2i
StepHypRef Expression
1 difeq1i.1 . 2 𝐴 = 𝐵
2 difeq2 4079 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  cdif 3916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-dif 3922
This theorem is referenced by:  difeq12i  4083  dfun3  4227  dfin3  4228  dfin4  4229  invdif  4230  indif  4231  difundi  4241  difindi  4243  difdif2  4246  dif32  4252  difabs  4253  dfsymdif3  4254  notrab  4265  dif0  4315  unvdif  4406  difdifdir  4420  dfif3  4464  difpr  4720  iinvdif  4988  cnvin  5990  fndifnfp  6929  dif1o  8121  dfsdom2  8637  dju1dif  9596  m1bits  15787  clsval2  21661  mretopd  21703  cmpfi  22019  llycmpkgen2  22161  pserdvlem2  25029  nbgrssvwo2  27158  finsumvtxdg2ssteplem1  27341  frgrwopreglem3  28105  iundifdifd  30327  iundifdif  30328  difres  30364  pmtrcnelor  30770  cycpmconjv  30819  cyc3conja  30834  sibfof  31658  eulerpartlemmf  31693  kur14lem2  32514  kur14lem6  32518  kur14lem7  32519  satfv1  32670  dfon4  33414  onint1  33857  bj-2upln1upl  34407  poimirlem8  35013  dfssr2  35847  prjspval2  39527  diophren  39674  nonrel  40204  dssmapntrcls  40754  salincl  42895  meaiuninc  43050  carageniuncllem1  43090
  Copyright terms: Public domain W3C validator