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

Theorem difeq2i 3291
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 3288 . 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 1623    \ cdif 3149
This theorem is referenced by:  difeq12i  3292  dfun3  3407  dfin3  3408  dfin4  3409  invdif  3410  indif  3411  difundi  3421  difindi  3423  dif32  3431  difabs  3432  symdif1  3433  notrab  3445  dif0  3524  undifv  3528  difdifdir  3541  dfif3  3575  cnvin  5088  dif1o  6499  dfsdom2  6984  dfsup3OLD  7197  cantnfp1lem1  7380  cantnfp1lem3  7382  oemapso  7384  cantnflem1d  7390  cantnflem1  7391  oef1o  7401  cnfcom2lem  7404  cda1dif  7802  m1bits  12631  clsval2  16787  mretopd  16829  cmpfi  17135  llycmpkgen2  17245  pserdvlem2  19804  kur14lem2  23738  kur14lem6  23742  kur14lem7  23743  dfon4  24433  onint1  24888  fndifnfp  26756  diophren  26896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-rab 2552  df-dif 3155
  Copyright terms: Public domain W3C validator