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

Theorem difeq2i 3459
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 3456 . 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 1362    \ cdif 3313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-rab 2714  df-dif 3319
This theorem is referenced by:  difeq12i  3460  dfun3  3576  dfin3  3577  dfin4  3578  invdif  3579  indif  3580  difundi  3590  difindi  3592  difdif2  3595  dif32  3601  difabs  3602  symdif1  3603  notrab  3615  dif0  3737  unvdif  3741  difdifdir  3754  dfif3  3791  iinvdif  4230  cnvin  5232  fndifnfp  5894  dif1o  6928  dfsdom2  7422  dfsup3OLD  7682  cantnffvalOLD  7859  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  cantnflem1dOLD  7907  cantnflem1OLD  7908  oef1oOLD  7919  cnfcom2lemOLD  7930  cda1dif  8333  m1bits  13618  clsval2  18495  mretopd  18537  cmpfi  18852  llycmpkgen2  18964  pserdvlem2  21777  iundifdifd  25735  iundifdif  25736  sibfof  26573  eulerpartlemmf  26605  kur14lem2  26942  kur14lem6  26946  kur14lem7  26947  dfon4  27770  onint1  28142  diophren  28994  difpr  29968  nbgrassvwo2  30120  clwlknclwlkdifs  30421  frgraregorufr0  30488  bj-2upln1upl  32097
  Copyright terms: Public domain W3C validator