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

Theorem difeq12d 3608
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 3606 . 2  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
3 difeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43difeq2d 3607 . 2  |-  ( ph  ->  ( B  \  C
)  =  ( B 
\  D ) )
52, 4eqtrd 2484 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    \ cdif 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rab 2802  df-dif 3464
This theorem is referenced by:  boxcutc  7514  unfilem3  7788  infdifsn  8076  cantnfp1lem3  8102  cantnfp1lem3OLD  8128  infcda1  8576  isf32lem6  8741  isf32lem7  8742  isf32lem8  8743  domtriomlem  8825  domtriom  8826  alephsuc3  8958  symgfixelsi  16438  pmtrprfval  16490  dprdf1o  17057  isirred  17326  isdrng  17378  isdrngd  17399  drngpropd  17401  issubdrg  17432  islbs  17700  lbspropd  17723  lssacsex  17768  lspsnat  17769  frlmlbs  18808  islindf  18824  lindfmm  18839  lsslindf  18842  ptcld  20091  iundisj  21935  iundisj2  21936  iunmbl  21940  volsup  21943  dchrval  23485  drngoi  25385  isdivrngo  25409  iundisjf  27424  iundisj2f  27425  iundisjfi  27577  iundisj2fi  27578  qtophaus  27816  zrhunitpreima  27936  meascnbl  28167  brae  28190  braew  28191  ballotlemfrc  28442  voliunnfl  30033  itg2addnclem  30041  stoweidlem34  31705  lsatset  34455  watfvalN  35456  mapdpglem26  37165  mapdpglem27  37166  hvmapffval  37225  hvmapfval  37226  hvmap1o2  37232
  Copyright terms: Public domain W3C validator