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

Theorem reseq12d 5088
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 5086 . 2  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
3 reseqd.2 . . 3  |-  ( ph  ->  C  =  D )
43reseq2d 5087 . 2  |-  ( ph  ->  ( B  |`  C )  =  ( B  |`  D ) )
52, 4eqtrd 2420 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    |` cres 4821
This theorem is referenced by:  oieq1  7415  oieq2  7416  ackbij2lem3  8055  setsvalg  13420  resfval  14017  resfval2  14018  resf2nd  14020  dpjfval  15541  psrval  16357  znval  16740  prdsdsf  18306  prdsxmet  18308  imasdsf1olem  18312  xpsxmetlem  18318  xpsmet  18321  isxms  18368  isms  18370  setsxms  18400  setsms  18401  ressxms  18446  ressms  18447  prdsxmslem2  18450  iscms  19168  cmsss  19173  minveclem3a  19196  dvcmulf  19699  efcvx  20233  ispth  21423  constr3pthlem1  21491  prdsbnd2  26196  cnpwstotbnd  26198  dfateq12d  27663  ldualset  29241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-in 3271  df-opab 4209  df-xp 4825  df-res 4831
  Copyright terms: Public domain W3C validator