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

Theorem reseq12d 5139
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 5137 . 2  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
3 reseqd.2 . . 3  |-  ( ph  ->  C  =  D )
43reseq2d 5138 . 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 4872
This theorem is referenced by:  oieq1  7473  oieq2  7474  ackbij2lem3  8113  setsvalg  13484  resfval  14081  resfval2  14082  resf2nd  14084  dpjfval  15605  psrval  16421  znval  16808  prdsdsf  18389  prdsxmet  18391  imasdsf1olem  18395  xpsxmetlem  18401  xpsmet  18404  isxms  18469  isms  18471  setsxms  18501  setsms  18502  ressxms  18547  ressms  18548  prdsxmslem2  18551  iscms  19290  cmsss  19295  minveclem3a  19320  dvcmulf  19823  efcvx  20357  ispth  21560  constr3pthlem1  21634  sitgclcn  24650  sitgclre  24651  prdsbnd2  26495  cnpwstotbnd  26497  dfateq12d  27960  ldualset  29860
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 4876  df-res 4882
  Copyright terms: Public domain W3C validator