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

Theorem reseq12d 5265
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 5263 . 2  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
3 reseqd.2 . . 3  |-  ( ph  ->  C  =  D )
43reseq2d 5264 . 2  |-  ( ph  ->  ( B  |`  C )  =  ( B  |`  D ) )
52, 4eqtrd 2501 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    |` cres 4994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-opab 4499  df-xp 4998  df-res 5004
This theorem is referenced by:  tfrlem3a  7036  oieq1  7926  oieq2  7927  ackbij2lem3  8610  setsvalg  14502  resfval  15108  resfval2  15109  resf2nd  15111  lubfval  15454  glbfval  15467  dpjfval  16887  psrval  17775  znval  18332  prdsdsf  20598  prdsxmet  20600  imasdsf1olem  20604  xpsxmetlem  20610  xpsmet  20613  isxms  20678  isms  20680  setsxms  20710  setsms  20711  ressxms  20756  ressms  20757  prdsxmslem2  20760  iscms  21512  cmsss  21517  minveclem3a  21570  dvcmulf  22076  efcvx  22571  ispth  24232  constr3pthlem1  24317  isrrext  27467  prdsbnd2  29745  cnpwstotbnd  29747  dvmptresicc  31068  itgcoscmulx  31106  fourierdlem73  31299  dfateq12d  31500  ldualset  33797
  Copyright terms: Public domain W3C validator