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

Theorem difeq12d 3470
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 3468 . 2  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
3 difeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43difeq2d 3469 . 2  |-  ( ph  ->  ( B  \  C
)  =  ( B 
\  D ) )
52, 4eqtrd 2470 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    \ cdif 3320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rab 2719  df-dif 3326
This theorem is referenced by:  boxcutc  7298  unfilem3  7570  infdifsn  7854  cantnfp1lem3  7880  cantnfp1lem3OLD  7906  infcda1  8354  isf32lem6  8519  isf32lem7  8520  isf32lem8  8521  domtriomlem  8603  domtriom  8604  alephsuc3  8736  symgfixelsi  15931  pmtrprfval  15984  dprdf1o  16517  isirred  16779  isdrng  16814  isdrngd  16835  drngpropd  16837  issubdrg  16868  islbs  17134  lbspropd  17157  lssacsex  17202  lspsnat  17203  frlmlbs  18200  islindf  18216  lindfmm  18231  lsslindf  18234  ptcld  19161  iundisj  21004  iundisj2  21005  iunmbl  21009  volsup  21012  dchrval  22548  drngoi  23845  isdivrngo  23869  iundisjf  25882  iundisj2f  25883  iundisjfi  26031  iundisj2fi  26032  zrhunitpreima  26359  meascnbl  26585  brae  26609  braew  26610  ballotlemfrc  26861  voliunnfl  28388  itg2addnclem  28396  stoweidlem34  29782  lsatset  32475  watfvalN  33476  mapdpglem26  35183  mapdpglem27  35184  hvmapffval  35243  hvmapfval  35244  hvmap1o2  35250
  Copyright terms: Public domain W3C validator