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

Theorem difeq12d 3295
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 3293 . 2  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
3 difeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43difeq2d 3294 . 2  |-  ( ph  ->  ( B  \  C
)  =  ( B 
\  D ) )
52, 4eqtrd 2315 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    \ cdif 3149
This theorem is referenced by:  boxcutc  6859  unfilem3  7123  infdifsn  7357  cantnfp1lem3  7382  infcda1  7819  isf32lem6  7984  isf32lem7  7985  isf32lem8  7986  domtriomlem  8068  domtriom  8069  alephsuc3  8202  dprdf1o  15267  isirred  15481  isdrng  15516  isdrngd  15537  drngpropd  15539  issubdrg  15570  islbs  15829  lbspropd  15852  lssacsex  15897  lspsnat  15898  ptcld  17307  iundisj  18905  iundisj2  18906  iunmbl  18910  volsup  18913  dchrval  20473  drngoi  21074  isdivrngo  21098  ballotlemfrc  23085  iundisjfi  23363  iundisj2fi  23364  iundisjf  23365  iundisj2f  23366  meascnbl  23546  difeq12dOLD  24967  frlmlbs  27249  islindf  27282  lindfmm  27297  lsslindf  27300  stoweidlem34  27783  lsatset  29180  watfvalN  30181  mapdpglem26  31888  mapdpglem27  31889  hvmapffval  31948  hvmapfval  31949  hvmap1o2  31955
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rab 2552  df-dif 3155
  Copyright terms: Public domain W3C validator