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

Theorem difeq12d 3458
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 3456 . 2  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
3 difeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43difeq2d 3457 . 2  |-  ( ph  ->  ( B  \  C
)  =  ( B 
\  D ) )
52, 4eqtrd 2467 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    \ cdif 3309
This theorem is referenced by:  boxcutc  7097  unfilem3  7365  infdifsn  7603  cantnfp1lem3  7628  infcda1  8065  isf32lem6  8230  isf32lem7  8231  isf32lem8  8232  domtriomlem  8314  domtriom  8315  alephsuc3  8447  dprdf1o  15582  isirred  15796  isdrng  15831  isdrngd  15852  drngpropd  15854  issubdrg  15885  islbs  16140  lbspropd  16163  lssacsex  16208  lspsnat  16209  ptcld  17637  iundisj  19434  iundisj2  19435  iunmbl  19439  volsup  19442  dchrval  21010  drngoi  21987  isdivrngo  22011  iundisjf  24021  iundisj2f  24022  iundisjfi  24144  iundisj2fi  24145  zrhunitpreima  24354  meascnbl  24565  brae  24584  braew  24585  ballotlemfrc  24776  voliunnfl  26240  itg2addnclem  26246  frlmlbs  27217  islindf  27250  lindfmm  27265  lsslindf  27268  stoweidlem34  27750  lsatset  29725  watfvalN  30726  mapdpglem26  32433  mapdpglem27  32434  hvmapffval  32493  hvmapfval  32494  hvmap1o2  32500
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 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rab 2706  df-dif 3315
  Copyright terms: Public domain W3C validator