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

Theorem reseq12d 4956
Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypotheses
Ref Expression
reseqd.1  |-  ( ph  ->  A  =  B )
reseqd.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
reseq12d  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  D ) )

Proof of Theorem reseq12d
StepHypRef Expression
1 reseqd.1 . . 3  |-  ( ph  ->  A  =  B )
21reseq1d 4954 . 2  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
3 reseqd.2 . . 3  |-  ( ph  ->  C  =  D )
43reseq2d 4955 . 2  |-  ( ph  ->  ( B  |`  C )  =  ( B  |`  D ) )
52, 4eqtrd 2315 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    |` cres 4691
This theorem is referenced by:  oieq1  7227  oieq2  7228  ackbij2lem3  7867  setsvalg  13171  resfval  13766  resfval2  13767  resf2nd  13769  dpjfval  15290  psrval  16110  znval  16489  prdsdsf  17931  prdsxmet  17933  imasdsf1olem  17937  xpsxmetlem  17943  xpsmet  17946  isxms  17993  isms  17995  setsxms  18025  setsms  18026  ressxms  18071  ressms  18072  prdsxmslem2  18075  iscms  18767  cmsss  18772  minveclem3a  18791  dvcmulf  19294  efcvx  19825  prdsbnd2  26519  cnpwstotbnd  26521  dfateq12d  27992  ldualset  29315
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-opab 4078  df-xp 4695  df-res 4701
  Copyright terms: Public domain W3C validator