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

Theorem reseq12d 5212
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 5210 . 2  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
3 reseqd.2 . . 3  |-  ( ph  ->  C  =  D )
43reseq2d 5211 . 2  |-  ( ph  ->  ( B  |`  C )  =  ( B  |`  D ) )
52, 4eqtrd 2492 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    |` cres 4943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-in 3436  df-opab 4452  df-xp 4947  df-res 4953
This theorem is referenced by:  tfrlem3a  6939  oieq1  7830  oieq2  7831  ackbij2lem3  8514  setsvalg  14308  resfval  14913  resfval2  14914  resf2nd  14916  lubfval  15259  glbfval  15272  dpjfval  16668  psrval  17544  znval  18084  prdsdsf  20067  prdsxmet  20069  imasdsf1olem  20073  xpsxmetlem  20079  xpsmet  20082  isxms  20147  isms  20149  setsxms  20179  setsms  20180  ressxms  20225  ressms  20226  prdsxmslem2  20229  iscms  20981  cmsss  20986  minveclem3a  21039  dvcmulf  21545  efcvx  22040  ispth  23612  constr3pthlem1  23686  isrrext  26567  prdsbnd2  28835  cnpwstotbnd  28837  dfateq12d  30176  ldualset  33079
  Copyright terms: Public domain W3C validator