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

Theorem difeq2i 3618
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 3615 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  \cdif 3472
This theorem is referenced by:  difeq12i  3619  dfun3  3735  dfin3  3736  dfin4  3737  invdif  3738  indif  3739  difundi  3749  difindi  3751  difdif2  3754  dif32  3760  difabs  3761  symdif1  3762  notrab  3774  dif0  3898  unvdif  3902  difdifdir  3915  dfif3  3955  difpr  4169  iinvdif  4402  cnvin  5418  fndifnfp  6100  dif1o  7169  dfsdom2  7660  dfsup3OLD  7924  cantnffvalOLD  8103  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  cantnflem1dOLD  8151  cantnflem1OLD  8152  oef1oOLD  8163  cnfcom2lemOLD  8174  cda1dif  8577  m1bits  14090  clsval2  19551  mretopd  19593  cmpfi  19908  llycmpkgen2  20051  pserdvlem2  22823  nbgrassvwo2  24438  clwlknclwlkdifs  24960  frgraregorufr0  25052  iundifdifd  27429  iundifdif  27430  difres  27457  sibfof  28282  eulerpartlemmf  28314  kur14lem2  28651  kur14lem6  28655  kur14lem7  28656  dfon4  29543  onint1  29914  diophren  30747  bj-2upln1upl  34582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-rab 2816  df-dif 3478
  Copyright terms: Public domain W3C validator