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

Theorem difeq12d 3691
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 3689 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 difeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43difeq2d 3690 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2644 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  cdif 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-dif 3543
This theorem is referenced by:  boxcutc  7837  unfilem3  8111  infdifsn  8437  cantnfp1lem3  8460  infcda1  8898  isf32lem6  9063  isf32lem7  9064  isf32lem8  9065  domtriomlem  9147  domtriom  9148  alephsuc3  9281  symgfixelsi  17678  pmtrprfval  17730  dprdf1o  18254  isirred  18522  isdrng  18574  isdrngd  18595  drngpropd  18597  issubdrg  18628  islbs  18897  lbspropd  18920  lssacsex  18965  lspsnat  18966  frlmlbs  19955  islindf  19970  lindfmm  19985  lsslindf  19988  ptcld  21226  iundisj  23123  iundisj2  23124  iunmbl  23128  volsup  23131  dchrval  24759  iundisjf  28784  iundisj2f  28785  iundisjfi  28942  iundisj2fi  28943  qtophaus  29231  zrhunitpreima  29350  meascnbl  29609  brae  29631  braew  29632  ballotlemfrc  29915  csbdif  32347  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem9  32588  poimirlem13  32592  poimirlem14  32593  poimirlem16  32595  poimirlem19  32598  voliunnfl  32623  itg2addnclem  32631  isdivrngo  32919  drngoi  32920  lsatset  33295  watfvalN  34296  mapdpglem26  36005  mapdpglem27  36006  hvmapffval  36065  hvmapfval  36066  hvmap1o2  36072  dssmapfvd  37331  fzdifsuc2  38466  stoweidlem34  38927  subsalsal  39253  iundjiunlem  39352  iundjiun  39353  meaiuninc  39374  carageniuncllem1  39411  carageniuncl  39413  hspdifhsp  39506  nbgrval  40560  nbgr1vtx  40580
  Copyright terms: Public domain W3C validator