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

Theorem difeq2i 3868
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 3865 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  cdif 3712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ral 3055  df-rab 3059  df-dif 3718
This theorem is referenced by:  difeq12i  3869  dfun3  4008  dfin3  4009  dfin4  4010  invdif  4011  indif  4012  difundi  4022  difindi  4024  difdif2  4027  dif32  4034  difabs  4035  dfsymdif3  4036  notrab  4047  dif0  4093  unvdif  4186  difdifdir  4200  dfif3  4244  difpr  4479  iinvdif  4744  cnvin  5698  fndifnfp  6607  dif1o  7751  dfsdom2  8250  cda1dif  9210  m1bits  15384  clsval2  21076  mretopd  21118  cmpfi  21433  llycmpkgen2  21575  pserdvlem2  24401  nbgrssvwo2  26478  nbgrssvwo2OLD  26481  finsumvtxdg2ssteplem1  26672  clwwlknclwwlkdifsOLD  27123  frgrwopreglem3  27489  iundifdifd  29708  iundifdif  29709  difres  29741  sibfof  30732  eulerpartlemmf  30767  kur14lem2  31517  kur14lem6  31521  kur14lem7  31522  dfon4  32327  onint1  32775  bj-2upln1upl  33336  poimirlem8  33748  dfssr2  34590  diophren  37897  nonrel  38410  dssmapntrcls  38946  salincl  41064  meaiuninc  41219  carageniuncllem1  41259
  Copyright terms: Public domain W3C validator