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

Theorem reseq12d 5260
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 5258 . 2  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
3 reseqd.2 . . 3  |-  ( ph  ->  C  =  D )
43reseq2d 5259 . 2  |-  ( ph  ->  ( B  |`  C )  =  ( B  |`  D ) )
52, 4eqtrd 2482 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    |` cres 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465  df-opab 4492  df-xp 4991  df-res 4997
This theorem is referenced by:  tfrlem3a  7044  oieq1  7935  oieq2  7936  ackbij2lem3  8619  setsvalg  14527  resfval  15130  resfval2  15131  resf2nd  15133  lubfval  15477  glbfval  15490  dpjfval  16972  psrval  17879  znval  18439  prdsdsf  20736  prdsxmet  20738  imasdsf1olem  20742  xpsxmetlem  20748  xpsmet  20751  isxms  20816  isms  20818  setsxms  20848  setsms  20849  ressxms  20894  ressms  20895  prdsxmslem2  20898  iscms  21650  cmsss  21655  minveclem3a  21708  dvcmulf  22214  efcvx  22709  ispth  24435  constr3pthlem1  24520  isrrext  27847  prdsbnd2  30259  cnpwstotbnd  30261  dvmptresicc  31616  itgcoscmulx  31654  fourierdlem73  31847  dfateq12d  32048  rngchomrnghmresOLD  32523  ldualset  34552
  Copyright terms: Public domain W3C validator