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

Theorem difeq12d 4097
Description: Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
Hypotheses
Ref Expression
difeq12d.1 (𝜑𝐴 = 𝐵)
difeq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
difeq12d (𝜑 → (𝐴𝐶) = (𝐵𝐷))

Proof of Theorem difeq12d
StepHypRef Expression
1 difeq12d.1 . . 3 (𝜑𝐴 = 𝐵)
21difeq1d 4095 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 difeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43difeq2d 4096 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2853 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cdif 3930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rab 3144  df-dif 3936
This theorem is referenced by:  boxcutc  8493  unfilem3  8772  infdifsn  9108  cantnfp1lem3  9131  isf32lem6  9768  isf32lem7  9769  isf32lem8  9770  domtriomlem  9852  domtriom  9853  alephsuc3  9990  symgfixelsi  18492  pmtrprfval  18544  dprdf1o  19083  isirred  19378  isdrng  19435  isdrngd  19456  drngpropd  19458  issubdrg  19489  subdrgint  19511  islbs  19777  lbspropd  19800  lssacsex  19845  lspsnat  19846  frlmlbs  20869  islindf  20884  lindfmm  20899  lsslindf  20902  ptcld  22149  iundisj  24076  iundisj2  24077  iunmbl  24081  volsup  24084  dchrval  25737  nbgrval  27045  nbgr1vtx  27067  iundisjf  30267  iundisj2f  30268  iundisjfi  30445  iundisj2fi  30446  lindfpropd  30869  sradrng  30887  qtophaus  30999  zrhunitpreima  31118  meascnbl  31377  brae  31399  braew  31400  ballotlemfrc  31683  reprdifc  31797  chtvalz  31799  satffunlem2lem2  32550  csbdif  34488  poimirlem4  34777  poimirlem6  34779  poimirlem7  34780  poimirlem9  34782  poimirlem13  34786  poimirlem14  34787  poimirlem16  34789  poimirlem19  34792  voliunnfl  34817  itg2addnclem  34824  isdivrngo  35109  drngoi  35110  lsatset  36006  watfvalN  37008  mapdpglem26  38714  mapdpglem27  38715  hvmapffval  38774  hvmapfval  38775  hvmap1o2  38781  prjspval  39131  dssmapfvd  40241  fzdifsuc2  41453  stoweidlem34  42196  subsalsal  42519  iundjiunlem  42618  iundjiun  42619  meaiuninc  42640  carageniuncllem1  42680  carageniuncl  42682  hspdifhsp  42775
  Copyright terms: Public domain W3C validator