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

Theorem reseq12d 5117
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 5115 . 2  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
3 reseqd.2 . . 3  |-  ( ph  ->  C  =  D )
43reseq2d 5116 . 2  |-  ( ph  ->  ( B  |`  C )  =  ( B  |`  D ) )
52, 4eqtrd 2461 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    |` cres 4847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-in 3440  df-opab 4476  df-xp 4851  df-res 4857
This theorem is referenced by:  tfrlem3a  7094  oieq1  8018  oieq2  8019  ackbij2lem3  8660  setsvalg  15105  resfval  15749  resfval2  15750  resf2nd  15752  lubfval  16176  glbfval  16189  dpjfval  17629  psrval  18527  znval  19043  prdsdsf  21319  prdsxmet  21321  imasdsf1olem  21325  xpsxmetlem  21331  xpsmet  21334  isxms  21399  isms  21401  setsxms  21431  setsms  21432  ressxms  21477  ressms  21478  prdsxmslem2  21481  iscms  22232  cmsss  22237  minveclem3a  22288  dvcmulf  22806  efcvx  23308  ispth  25184  constr3pthlem1  25269  padct  28191  isrrext  28684  prdsbnd2  31875  cnpwstotbnd  31877  ldualset  32444  dvmptresicc  37411  itgcoscmulx  37463  fourierdlem73  37659  sge0fodjrnlem  37840  dfateq12d  38078  rngchomrnghmresALTV  38813  fdivval  39168
  Copyright terms: Public domain W3C validator