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

Theorem funssfv 5688
Description: The value of a member of the domain of a subclass of a function. (Contributed by NM, 15-Aug-1994.)
Assertion
Ref Expression
funssfv  |-  ( ( Fun  F  /\  G  C_  F  /\  A  e. 
dom  G )  -> 
( F `  A
)  =  ( G `
 A ) )

Proof of Theorem funssfv
StepHypRef Expression
1 fvres 5687 . . . 4  |-  ( A  e.  dom  G  -> 
( ( F  |`  dom  G ) `  A
)  =  ( F `
 A ) )
21eqcomd 2394 . . 3  |-  ( A  e.  dom  G  -> 
( F `  A
)  =  ( ( F  |`  dom  G ) `
 A ) )
3 funssres 5435 . . . 4  |-  ( ( Fun  F  /\  G  C_  F )  ->  ( F  |`  dom  G )  =  G )
43fveq1d 5672 . . 3  |-  ( ( Fun  F  /\  G  C_  F )  ->  (
( F  |`  dom  G
) `  A )  =  ( G `  A ) )
52, 4sylan9eqr 2443 . 2  |-  ( ( ( Fun  F  /\  G  C_  F )  /\  A  e.  dom  G )  ->  ( F `  A )  =  ( G `  A ) )
653impa 1148 1  |-  ( ( Fun  F  /\  G  C_  F  /\  A  e. 
dom  G )  -> 
( F `  A
)  =  ( G `
 A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1717    C_ wss 3265   dom cdm 4820    |` cres 4822   Fun wfun 5390   ` cfv 5396
This theorem is referenced by:  tfrlem9  6584  tfrlem11  6587  ac6sfi  7289  axdc3lem2  8266  axdc3lem4  8268  imasvscaval  13692  pserdv  20214  eupap1  21548  sspn  22085  subfacp1lem2a  24647  subfacp1lem2b  24648  subfacp1lem5  24651  cvmliftlem10  24762  cvmliftlem13  24764  wfrlem12  25293  wfrlem14  25295  frrlem11  25319  bnj945  28484  bnj1502  28559  bnj545  28606  bnj548  28608
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-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-res 4832  df-iota 5360  df-fun 5398  df-fv 5404
  Copyright terms: Public domain W3C validator