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

Theorem difeq2i 3304
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 3301 . 2  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
31, 2ax-mp 8 1  |-  ( C 
\  A )  =  ( C  \  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1632    \ cdif 3162
This theorem is referenced by:  difeq12i  3305  dfun3  3420  dfin3  3421  dfin4  3422  invdif  3423  indif  3424  difundi  3434  difindi  3436  dif32  3444  difabs  3445  symdif1  3446  notrab  3458  dif0  3537  undifv  3541  difdifdir  3554  dfif3  3588  cnvin  5104  dif1o  6515  dfsdom2  7000  dfsup3OLD  7213  cantnfp1lem1  7396  cantnfp1lem3  7398  oemapso  7400  cantnflem1d  7406  cantnflem1  7407  oef1o  7417  cnfcom2lem  7420  cda1dif  7818  m1bits  12647  clsval2  16803  mretopd  16845  cmpfi  17151  llycmpkgen2  17261  pserdvlem2  19820  kur14lem2  23753  kur14lem6  23757  kur14lem7  23758  dfon4  24504  onint1  24960  fndifnfp  26859  diophren  26999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-rab 2565  df-dif 3168
  Copyright terms: Public domain W3C validator