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

Theorem difeq2i 3619
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 3616 . 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 1379    \ cdif 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-rab 2823  df-dif 3479
This theorem is referenced by:  difeq12i  3620  dfun3  3736  dfin3  3737  dfin4  3738  invdif  3739  indif  3740  difundi  3750  difindi  3752  difdif2  3755  dif32  3761  difabs  3762  symdif1  3763  notrab  3775  dif0  3897  unvdif  3901  difdifdir  3914  dfif3  3953  difpr  4166  iinvdif  4397  cnvin  5411  fndifnfp  6088  dif1o  7147  dfsdom2  7637  dfsup3OLD  7900  cantnffvalOLD  8078  cantnfp1lem1OLD  8119  cantnfp1lem3OLD  8121  cantnflem1dOLD  8126  cantnflem1OLD  8127  oef1oOLD  8138  cnfcom2lemOLD  8149  cda1dif  8552  m1bits  13945  clsval2  19317  mretopd  19359  cmpfi  19674  llycmpkgen2  19786  pserdvlem2  22557  nbgrassvwo2  24114  clwlknclwlkdifs  24636  frgraregorufr0  24729  iundifdifd  27102  iundifdif  27103  difres  27130  sibfof  27922  eulerpartlemmf  27954  kur14lem2  28291  kur14lem6  28295  kur14lem7  28296  dfon4  29120  onint1  29491  diophren  30351  bj-2upln1upl  33663
  Copyright terms: Public domain W3C validator