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

Theorem difeq2i 3462
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 3459 . 2  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
31, 2ax-mp 8 1  |-  ( C 
\  A )  =  ( C  \  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    \ cdif 3317
This theorem is referenced by:  difeq12i  3463  dfun3  3579  dfin3  3580  dfin4  3581  invdif  3582  indif  3583  difundi  3593  difindi  3595  difdif2  3598  dif32  3604  difabs  3605  symdif1  3606  notrab  3618  dif0  3698  undifv  3702  difdifdir  3715  dfif3  3749  cnvin  5279  dif1o  6744  dfsdom2  7230  dfsup3OLD  7449  cantnfp1lem1  7634  cantnfp1lem3  7636  oemapso  7638  cantnflem1d  7644  cantnflem1  7645  oef1o  7655  cnfcom2lem  7658  cda1dif  8056  m1bits  12952  clsval2  17114  mretopd  17156  cmpfi  17471  llycmpkgen2  17582  pserdvlem2  20344  iundifdifd  24012  iundifdif  24013  sibfof  24654  kur14lem2  24893  kur14lem6  24897  kur14lem7  24898  dfon4  25738  onint1  26199  fndifnfp  26737  diophren  26874  frgraregorufr0  28441
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-ral 2710  df-rab 2714  df-dif 3323
  Copyright terms: Public domain W3C validator