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

Theorem reseq12d 4972
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 4970 . 2  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
3 reseqd.2 . . 3  |-  ( ph  ->  C  =  D )
43reseq2d 4971 . 2  |-  ( ph  ->  ( B  |`  C )  =  ( B  |`  D ) )
52, 4eqtrd 2328 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    |` cres 4707
This theorem is referenced by:  oieq1  7243  oieq2  7244  ackbij2lem3  7883  setsvalg  13187  resfval  13782  resfval2  13783  resf2nd  13785  dpjfval  15306  psrval  16126  znval  16505  prdsdsf  17947  prdsxmet  17949  imasdsf1olem  17953  xpsxmetlem  17959  xpsmet  17962  isxms  18009  isms  18011  setsxms  18041  setsms  18042  ressxms  18087  ressms  18088  prdsxmslem2  18091  iscms  18783  cmsss  18788  minveclem3a  18807  dvcmulf  19310  efcvx  19841  prdsbnd2  26622  cnpwstotbnd  26624  dfateq12d  28097  ispth  28354  constr3pthlem1  28401  ldualset  29937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-opab 4094  df-xp 4711  df-res 4717
  Copyright terms: Public domain W3C validator