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

Theorem difeq2i 3571
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 3568 . 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 1370    \ cdif 3425
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-ral 2800  df-rab 2804  df-dif 3431
This theorem is referenced by:  difeq12i  3572  dfun3  3688  dfin3  3689  dfin4  3690  invdif  3691  indif  3692  difundi  3702  difindi  3704  difdif2  3707  dif32  3713  difabs  3714  symdif1  3715  notrab  3727  dif0  3849  unvdif  3853  difdifdir  3866  dfif3  3903  iinvdif  4342  cnvin  5344  fndifnfp  6008  dif1o  7042  dfsdom2  7536  dfsup3OLD  7797  cantnffvalOLD  7974  cantnfp1lem1OLD  8015  cantnfp1lem3OLD  8017  cantnflem1dOLD  8022  cantnflem1OLD  8023  oef1oOLD  8034  cnfcom2lemOLD  8045  cda1dif  8448  m1bits  13740  clsval2  18772  mretopd  18814  cmpfi  19129  llycmpkgen2  19241  pserdvlem2  22011  iundifdifd  26048  iundifdif  26049  sibfof  26862  eulerpartlemmf  26894  kur14lem2  27231  kur14lem6  27235  kur14lem7  27236  dfon4  28060  onint1  28431  diophren  29292  difpr  30265  nbgrassvwo2  30417  clwlknclwlkdifs  30718  frgraregorufr0  30785  bj-2upln1upl  32819
  Copyright terms: Public domain W3C validator