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

Theorem difeq12d 4084
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 4082 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 difeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43difeq2d 4083 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2773 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cdif 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-dif 3914
This theorem is referenced by:  csbdif  4486  xpord2pred  8078  xpord3pred  8085  boxcutc  8882  unfilem3  9259  infdifsn  9598  cantnfp1lem3  9621  isf32lem6  10299  isf32lem7  10300  isf32lem8  10301  domtriomlem  10383  domtriom  10384  alephsuc3  10521  symgfixelsi  19222  pmtrprfval  19274  dprdf1o  19816  isirred  20135  isdrng  20201  isdrngd  20226  isdrngdOLD  20228  drngpropd  20230  issubdrg  20261  subdrgint  20284  islbs  20552  lbspropd  20575  lssacsex  20621  lspsnat  20622  frlmlbs  21219  islindf  21234  lindfmm  21249  lsslindf  21252  ptcld  22980  iundisj  24928  iundisj2  24929  iunmbl  24933  volsup  24936  dchrval  26598  newval  27207  sltlpss  27258  nbgrval  28326  nbgr1vtx  28348  iundisjf  31553  iundisj2f  31554  iundisjfi  31746  iundisj2fi  31747  lindfpropd  32217  rprmval  32309  sradrng  32342  qtophaus  32474  zrhunitpreima  32616  meascnbl  32875  brae  32897  braew  32898  ballotlemfrc  33183  reprdifc  33297  chtvalz  33299  satffunlem2lem2  34057  poimirlem4  36128  poimirlem6  36130  poimirlem7  36131  poimirlem9  36133  poimirlem13  36137  poimirlem14  36138  poimirlem16  36140  poimirlem19  36143  voliunnfl  36168  itg2addnclem  36175  isdivrngo  36455  drngoi  36456  lsatset  37498  watfvalN  38501  mapdpglem26  40207  mapdpglem27  40208  hvmapffval  40267  hvmapfval  40268  hvmap1o2  40274  prjspval  40984  prjspnvs  41001  cantnfresb  41702  dssmapfvd  42377  fzdifsuc2  43631  stoweidlem34  44361  subsalsal  44686  iundjiunlem  44786  iundjiun  44787  meaiuninc  44808  carageniuncllem1  44848  carageniuncl  44850  hspdifhsp  44943
  Copyright terms: Public domain W3C validator