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

Theorem difeq12d 3426
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 3424 . 2  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
3 difeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43difeq2d 3425 . 2  |-  ( ph  ->  ( B  \  C
)  =  ( B 
\  D ) )
52, 4eqtrd 2436 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    \ cdif 3277
This theorem is referenced by:  boxcutc  7064  unfilem3  7332  infdifsn  7567  cantnfp1lem3  7592  infcda1  8029  isf32lem6  8194  isf32lem7  8195  isf32lem8  8196  domtriomlem  8278  domtriom  8279  alephsuc3  8411  dprdf1o  15545  isirred  15759  isdrng  15794  isdrngd  15815  drngpropd  15817  issubdrg  15848  islbs  16103  lbspropd  16126  lssacsex  16171  lspsnat  16172  ptcld  17598  iundisj  19395  iundisj2  19396  iunmbl  19400  volsup  19403  dchrval  20971  drngoi  21948  isdivrngo  21972  iundisjf  23982  iundisj2f  23983  iundisjfi  24105  iundisj2fi  24106  zrhunitpreima  24315  meascnbl  24526  brae  24545  braew  24546  ballotlemfrc  24737  voliunnfl  26149  itg2addnclem  26155  frlmlbs  27117  islindf  27150  lindfmm  27165  lsslindf  27168  stoweidlem34  27650  lsatset  29473  watfvalN  30474  mapdpglem26  32181  mapdpglem27  32182  hvmapffval  32241  hvmapfval  32242  hvmap1o2  32248
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rab 2675  df-dif 3283
  Copyright terms: Public domain W3C validator