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

Theorem difeq2i 3687
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 3684 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  cdif 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-rab 2905  df-dif 3543
This theorem is referenced by:  difeq12i  3688  dfun3  3824  dfin3  3825  dfin4  3826  invdif  3827  indif  3828  difundi  3838  difindi  3840  difdif2  3843  dif32  3850  difabs  3851  dfsymdif3  3852  notrab  3863  dif0  3904  unvdif  3994  difdifdir  4008  dfif3  4050  difpr  4275  iinvdif  4528  cnvin  5459  fndifnfp  6347  dif1o  7467  dfsdom2  7968  cda1dif  8881  m1bits  15000  clsval2  20664  mretopd  20706  cmpfi  21021  llycmpkgen2  21163  pserdvlem2  23986  nbgrassvwo2  25967  clwlknclwlkdifs  26487  frgraregorufr0  26579  iundifdifd  28762  iundifdif  28763  difres  28795  sibfof  29729  eulerpartlemmf  29764  kur14lem2  30443  kur14lem6  30447  kur14lem7  30448  dfon4  31170  onint1  31618  bj-2upln1upl  32205  poimirlem8  32587  diophren  36395  nonrel  36909  dssmapntrcls  37446  salincl  39219  meaiuninc  39374  carageniuncllem1  39411  nbgrssvwo2  40587  clwwlknclwwlkdifs  41181  frgrregorufr0  41489
  Copyright terms: Public domain W3C validator