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

Theorem difeq2i 4080
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 4077 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cdif 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-dif 3914
This theorem is referenced by:  difeq12i  4081  dfun3  4226  dfin3  4227  dfin4  4228  invdif  4229  indif  4230  difundi  4240  difindi  4242  difdif2  4247  dif32  4253  difabs  4254  dfsymdif3  4257  notrab  4272  dif0  4333  unvdif  4435  difdifdir  4450  dfif3  4501  difpr  4764  iinvdif  5041  cnvin  6098  fndifnfp  7123  dif1o  8447  dfsdom2  9043  brttrcl2  9655  ttrcltr  9657  rnttrcl  9663  dju1dif  10113  m1bits  16325  clsval2  22417  mretopd  22459  cmpfi  22775  llycmpkgen2  22917  pserdvlem2  25803  nbgrssvwo2  28352  finsumvtxdg2ssteplem1  28535  frgrwopreglem3  29300  iundifdifd  31526  iundifdif  31527  difres  31564  gsumhashmul  31947  pmtrcnelor  31991  cycpmconjv  32040  cyc3conja  32055  sibfof  32997  eulerpartlemmf  33032  kur14lem2  33858  kur14lem6  33862  kur14lem7  33863  satfv1  34014  dfon4  34524  onint1  34967  bj-2upln1upl  35541  poimirlem8  36132  dfssr2  37007  prjspval2  40994  diophren  41179  ordeldif1o  41638  nonrel  41944  dssmapntrcls  42488  salincl  44651  meaiuninc  44808  carageniuncllem1  44848  iscnrm3rlem3  47061
  Copyright terms: Public domain W3C validator