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

Theorem difeq2i 3580
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 3577 . 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 1437    \ cdif 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-ral 2776  df-rab 2780  df-dif 3439
This theorem is referenced by:  difeq12i  3581  dfun3  3711  dfin3  3712  dfin4  3713  invdif  3714  indif  3715  difundi  3725  difindi  3727  difdif2  3730  dif32  3736  difabs  3737  dfsymdif3  3738  symdif1OLD  3739  notrab  3750  dif0  3867  unvdif  3871  difdifdir  3885  dfif3  3925  difpr  4139  iinvdif  4371  cnvin  5262  fndifnfp  6108  dif1o  7213  dfsdom2  7704  cda1dif  8613  m1bits  14413  clsval2  20063  mretopd  20106  cmpfi  20421  llycmpkgen2  20563  pserdvlem2  23381  nbgrassvwo2  25164  clwlknclwlkdifs  25686  frgraregorufr0  25778  iundifdifd  28179  iundifdif  28180  difres  28213  sibfof  29181  eulerpartlemmf  29216  kur14lem2  29938  kur14lem6  29942  kur14lem7  29943  dfon4  30665  onint1  31114  bj-2upln1upl  31586  poimirlem8  31912  diophren  35625  nonrel  36160  salincl  38105  carageniuncllem1  38250  nbgrssvwo2  39198
  Copyright terms: Public domain W3C validator