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

Theorem difeq2i 3605
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 3602 . 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 1398    \ cdif 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2809  df-rab 2813  df-dif 3464
This theorem is referenced by:  difeq12i  3606  dfun3  3733  dfin3  3734  dfin4  3735  invdif  3736  indif  3737  difundi  3747  difindi  3749  difdif2  3752  dif32  3758  difabs  3759  dfsymdif3  3760  symdif1OLD  3761  notrab  3772  dif0  3886  unvdif  3890  difdifdir  3903  dfif3  3943  difpr  4155  iinvdif  4387  cnvin  5398  fndifnfp  6076  dif1o  7142  dfsdom2  7633  cantnffvalOLD  8073  cantnfp1lem1OLD  8114  cantnfp1lem3OLD  8116  cantnflem1dOLD  8121  cantnflem1OLD  8122  oef1oOLD  8133  cnfcom2lemOLD  8144  cda1dif  8547  m1bits  14177  clsval2  19721  mretopd  19763  cmpfi  20078  llycmpkgen2  20220  pserdvlem2  22992  nbgrassvwo2  24643  clwlknclwlkdifs  25165  frgraregorufr0  25257  iundifdifd  27642  iundifdif  27643  difres  27674  sibfof  28549  eulerpartlemmf  28581  kur14lem2  28918  kur14lem6  28922  kur14lem7  28923  dfon4  29774  onint1  30145  diophren  30989  bj-2upln1upl  35002
  Copyright terms: Public domain W3C validator