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

Theorem difeq12d 3576
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 3574 . 2  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
3 difeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43difeq2d 3575 . 2  |-  ( ph  ->  ( B  \  C
)  =  ( B 
\  D ) )
52, 4eqtrd 2492 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    \ cdif 3426
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-nfc 2601  df-ral 2800  df-rab 2804  df-dif 3432
This theorem is referenced by:  boxcutc  7409  unfilem3  7682  infdifsn  7966  cantnfp1lem3  7992  cantnfp1lem3OLD  8018  infcda1  8466  isf32lem6  8631  isf32lem7  8632  isf32lem8  8633  domtriomlem  8715  domtriom  8716  alephsuc3  8848  symgfixelsi  16051  pmtrprfval  16104  dprdf1o  16643  isirred  16906  isdrng  16951  isdrngd  16972  drngpropd  16974  issubdrg  17005  islbs  17272  lbspropd  17295  lssacsex  17340  lspsnat  17341  frlmlbs  18343  islindf  18359  lindfmm  18374  lsslindf  18377  ptcld  19311  iundisj  21155  iundisj2  21156  iunmbl  21160  volsup  21163  dchrval  22699  drngoi  24039  isdivrngo  24063  iundisjf  26075  iundisj2f  26076  iundisjfi  26218  iundisj2fi  26219  zrhunitpreima  26545  meascnbl  26771  brae  26794  braew  26795  ballotlemfrc  27046  voliunnfl  28576  itg2addnclem  28584  stoweidlem34  29970  lsatset  32944  watfvalN  33945  mapdpglem26  35652  mapdpglem27  35653  hvmapffval  35712  hvmapfval  35713  hvmap1o2  35719
  Copyright terms: Public domain W3C validator