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

Theorem difeq2i 3586
Description: Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1i.1  |-  A  =  B
Assertion
Ref Expression
difeq2i  |-  ( C 
\  A )  =  ( C  \  B
)

Proof of Theorem difeq2i
StepHypRef Expression
1 difeq1i.1 . 2  |-  A  =  B
2 difeq2 3583 . 2  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
31, 2ax-mp 5 1  |-  ( C 
\  A )  =  ( C  \  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    \ cdif 3439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-ral 2787  df-rab 2791  df-dif 3445
This theorem is referenced by:  difeq12i  3587  dfun3  3717  dfin3  3718  dfin4  3719  invdif  3720  indif  3721  difundi  3731  difindi  3733  difdif2  3736  dif32  3742  difabs  3743  dfsymdif3  3744  symdif1OLD  3745  notrab  3756  dif0  3871  unvdif  3875  difdifdir  3889  dfif3  3929  difpr  4142  iinvdif  4374  cnvin  5263  fndifnfp  6108  dif1o  7210  dfsdom2  7701  cda1dif  8604  m1bits  14388  clsval2  19996  mretopd  20039  cmpfi  20354  llycmpkgen2  20496  pserdvlem2  23248  nbgrassvwo2  25011  clwlknclwlkdifs  25533  frgraregorufr0  25625  iundifdifd  28016  iundifdif  28017  difres  28050  sibfof  29001  eulerpartlemmf  29034  kur14lem2  29718  kur14lem6  29722  kur14lem7  29723  dfon4  30445  onint1  30894  bj-2upln1upl  31367  poimirlem8  31651  diophren  35364  salincl  37730  carageniuncllem1  37850
  Copyright terms: Public domain W3C validator