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

Theorem difeq12d 3308
Description: Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
Hypotheses
Ref Expression
difeq12d.1  |-  ( ph  ->  A  =  B )
difeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
difeq12d  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )

Proof of Theorem difeq12d
StepHypRef Expression
1 difeq12d.1 . . 3  |-  ( ph  ->  A  =  B )
21difeq1d 3306 . 2  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
3 difeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43difeq2d 3307 . 2  |-  ( ph  ->  ( B  \  C
)  =  ( B 
\  D ) )
52, 4eqtrd 2328 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    \ cdif 3162
This theorem is referenced by:  boxcutc  6875  unfilem3  7139  infdifsn  7373  cantnfp1lem3  7398  infcda1  7835  isf32lem6  8000  isf32lem7  8001  isf32lem8  8002  domtriomlem  8084  domtriom  8085  alephsuc3  8218  dprdf1o  15283  isirred  15497  isdrng  15532  isdrngd  15553  drngpropd  15555  issubdrg  15586  islbs  15845  lbspropd  15868  lssacsex  15913  lspsnat  15914  ptcld  17323  iundisj  18921  iundisj2  18922  iunmbl  18926  volsup  18929  dchrval  20489  drngoi  21090  isdivrngo  21114  ballotlemfrc  23101  iundisjfi  23378  iundisj2fi  23379  iundisjf  23380  iundisj2f  23381  meascnbl  23561  itg2addnclem  25003  difeq12dOLD  25070  frlmlbs  27352  islindf  27385  lindfmm  27400  lsslindf  27403  stoweidlem34  27886  lsatset  29802  watfvalN  30803  mapdpglem26  32510  mapdpglem27  32511  hvmapffval  32570  hvmapfval  32571  hvmap1o2  32577
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rab 2565  df-dif 3168
  Copyright terms: Public domain W3C validator