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

Theorem difeq2i 3537
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 3534 . 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 1452    \ cdif 3387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-ral 2761  df-rab 2765  df-dif 3393
This theorem is referenced by:  difeq12i  3538  dfun3  3672  dfin3  3673  dfin4  3674  invdif  3675  indif  3676  difundi  3686  difindi  3688  difdif2  3691  dif32  3697  difabs  3698  dfsymdif3  3699  symdif1OLD  3700  notrab  3711  dif0  3749  unvdif  3832  difdifdir  3846  dfif3  3886  difpr  4102  iinvdif  4341  cnvin  5249  fndifnfp  6109  dif1o  7220  dfsdom2  7713  cda1dif  8624  m1bits  14493  clsval2  20142  mretopd  20185  cmpfi  20500  llycmpkgen2  20642  pserdvlem2  23462  nbgrassvwo2  25245  clwlknclwlkdifs  25767  frgraregorufr0  25859  iundifdifd  28254  iundifdif  28255  difres  28287  sibfof  29246  eulerpartlemmf  29281  kur14lem2  30002  kur14lem6  30006  kur14lem7  30007  dfon4  30731  onint1  31180  bj-2upln1upl  31688  poimirlem8  32012  diophren  35727  nonrel  36261  salincl  38296  carageniuncllem1  38461  nbgrssvwo2  39597
  Copyright terms: Public domain W3C validator