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

Theorem difeq12d 3402
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 3400 . 2  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
3 difeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43difeq2d 3401 . 2  |-  ( ph  ->  ( B  \  C
)  =  ( B 
\  D ) )
52, 4eqtrd 2412 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    \ cdif 3253
This theorem is referenced by:  boxcutc  7034  unfilem3  7302  infdifsn  7537  cantnfp1lem3  7562  infcda1  7999  isf32lem6  8164  isf32lem7  8165  isf32lem8  8166  domtriomlem  8248  domtriom  8249  alephsuc3  8381  dprdf1o  15510  isirred  15724  isdrng  15759  isdrngd  15780  drngpropd  15782  issubdrg  15813  islbs  16068  lbspropd  16091  lssacsex  16136  lspsnat  16137  ptcld  17559  iundisj  19302  iundisj2  19303  iunmbl  19307  volsup  19310  dchrval  20878  drngoi  21836  isdivrngo  21860  iundisjf  23865  iundisj2f  23866  iundisjfi  23983  iundisj2fi  23984  zrhunitpreima  24154  meascnbl  24360  brae  24379  braew  24380  ballotlemfrc  24556  voliunnfl  25948  itg2addnclem  25950  frlmlbs  26911  islindf  26944  lindfmm  26959  lsslindf  26962  stoweidlem34  27444  lsatset  29156  watfvalN  30157  mapdpglem26  31864  mapdpglem27  31865  hvmapffval  31924  hvmapfval  31925  hvmap1o2  31931
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ral 2647  df-rab 2651  df-dif 3259
  Copyright terms: Public domain W3C validator