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

Theorem difeq12d 3623
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 3621 . 2  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
3 difeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43difeq2d 3622 . 2  |-  ( ph  ->  ( B  \  C
)  =  ( B 
\  D ) )
52, 4eqtrd 2508 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    \ cdif 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rab 2823  df-dif 3479
This theorem is referenced by:  boxcutc  7509  unfilem3  7782  infdifsn  8069  cantnfp1lem3  8095  cantnfp1lem3OLD  8121  infcda1  8569  isf32lem6  8734  isf32lem7  8735  isf32lem8  8736  domtriomlem  8818  domtriom  8819  alephsuc3  8951  symgfixelsi  16255  pmtrprfval  16308  dprdf1o  16869  isirred  17132  isdrng  17183  isdrngd  17204  drngpropd  17206  issubdrg  17237  islbs  17505  lbspropd  17528  lssacsex  17573  lspsnat  17574  frlmlbs  18598  islindf  18614  lindfmm  18629  lsslindf  18632  ptcld  19849  iundisj  21693  iundisj2  21694  iunmbl  21698  volsup  21701  dchrval  23237  drngoi  25085  isdivrngo  25109  iundisjf  27121  iundisj2f  27122  iundisjfi  27269  iundisj2fi  27270  zrhunitpreima  27595  qtophaus  27637  meascnbl  27830  brae  27853  braew  27854  ballotlemfrc  28105  voliunnfl  29635  itg2addnclem  29643  stoweidlem34  31334  lsatset  33787  watfvalN  34788  mapdpglem26  36495  mapdpglem27  36496  hvmapffval  36555  hvmapfval  36556  hvmap1o2  36562
  Copyright terms: Public domain W3C validator