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

Theorem reseq12d 5138
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 5136 . 2  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
3 reseqd.2 . . 3  |-  ( ph  ->  C  =  D )
43reseq2d 5137 . 2  |-  ( ph  ->  ( B  |`  C )  =  ( B  |`  D ) )
52, 4eqtrd 2467 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    |` cres 4871
This theorem is referenced by:  oieq1  7470  oieq2  7471  ackbij2lem3  8110  setsvalg  13480  resfval  14077  resfval2  14078  resf2nd  14080  dpjfval  15601  psrval  16417  znval  16804  prdsdsf  18385  prdsxmet  18387  imasdsf1olem  18391  xpsxmetlem  18397  xpsmet  18400  isxms  18465  isms  18467  setsxms  18497  setsms  18498  ressxms  18543  ressms  18544  prdsxmslem2  18547  iscms  19286  cmsss  19291  minveclem3a  19316  dvcmulf  19819  efcvx  20353  ispth  21556  constr3pthlem1  21630  sitgclcn  24646  sitgclre  24647  prdsbnd2  26441  cnpwstotbnd  26443  dfateq12d  27907  ldualset  29762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-opab 4259  df-xp 4875  df-res 4881
  Copyright terms: Public domain W3C validator