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

Theorem fvmptd 5810
Description: Deduction version of fvmpt 5806. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fvmptd.1  |-  ( ph  ->  F  =  ( x  e.  D  |->  B ) )
fvmptd.2  |-  ( (
ph  /\  x  =  A )  ->  B  =  C )
fvmptd.3  |-  ( ph  ->  A  e.  D )
fvmptd.4  |-  ( ph  ->  C  e.  V )
Assertion
Ref Expression
fvmptd  |-  ( ph  ->  ( F `  A
)  =  C )
Distinct variable groups:    x, A    x, C    x, D    ph, x
Allowed substitution hints:    B( x)    F( x)    V( x)

Proof of Theorem fvmptd
StepHypRef Expression
1 fvmptd.1 . . 3  |-  ( ph  ->  F  =  ( x  e.  D  |->  B ) )
21fveq1d 5730 . 2  |-  ( ph  ->  ( F `  A
)  =  ( ( x  e.  D  |->  B ) `  A ) )
3 fvmptd.3 . . 3  |-  ( ph  ->  A  e.  D )
4 fvmptd.2 . . . . 5  |-  ( (
ph  /\  x  =  A )  ->  B  =  C )
53, 4csbied 3293 . . . 4  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
6 fvmptd.4 . . . 4  |-  ( ph  ->  C  e.  V )
75, 6eqeltrd 2510 . . 3  |-  ( ph  ->  [_ A  /  x ]_ B  e.  V
)
8 eqid 2436 . . . 4  |-  ( x  e.  D  |->  B )  =  ( x  e.  D  |->  B )
98fvmpts 5807 . . 3  |-  ( ( A  e.  D  /\  [_ A  /  x ]_ B  e.  V )  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
103, 7, 9syl2anc 643 . 2  |-  ( ph  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
112, 10, 53eqtrd 2472 1  |-  ( ph  ->  ( F `  A
)  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   [_csb 3251    e. cmpt 4266   ` cfv 5454
This theorem is referenced by:  fvmptdv2  5818  ttukeylem3  8391  ccatval1  11745  ccatval2  11746  prdsvscafval  13702  mrcval  13835  cidval  13902  subcid  14044  idfu2nd  14074  resf2nd  14092  fuccoval  14160  fucid  14168  homaval  14186  idaval  14213  setcval  14232  setcid  14241  catcval  14251  catcid  14258  prf1  14297  prf2  14299  curf1  14322  curf11  14323  curf2val  14327  hofval  14349  hof2  14354  yonval  14358  yonedalem4a  14372  frmdval  14796  vrmdval  14802  gexval  15212  pj1val  15327  dpjval  15614  sraval  16248  opsrval  16535  lmfval  17296  kgenval  17567  ptval  17602  fcfval  18065  cnextfval  18093  ustval  18232  utopval  18262  ustuqtoplem  18269  utopsnneiplem  18277  tusval  18296  blfvalps  18413  tmsval  18511  metuvalOLD  18579  metuval  18580  caufval  19228  taylpval  20283  logexprlim  21009  dchrval  21018  dchr1  21041  metidval  24285  pstmval  24290  qqhvval  24367  indv  24410  indval  24411  indfval  24414  esummulc1  24471  esumcvg  24476  ofcval  24482  sigagenval  24523  measinb  24575  sitgfval  24655  totprobd  24684  probmeasb  24688  cndprobval  24691  dstrvprob  24729  dstfrvinc  24734  dstfrvclim1  24735  ballotlemfval  24747  ballotlemsv  24767  lgamgulmlem2  24814  lgamcvglem  24824  cvmliftlem9  24980  relexp0  25129  relexpsucr  25130  rtrclreclem.subset  25145  rtrclreclem.min  25147  dfrtrcl2  25148  mblfinlem2  26244  areacirc  26297  fmuldfeqlem1  27688  clim1fr1  27703  climrec  27705  climexp  27707  climneg  27712  itgsinexp  27725  stoweidlem7  27732  stoweidlem17  27742  stoweidlem32  27757  stoweidlem34  27759  wallispilem4  27793  wallispilem5  27794  wallispi  27795  wallispi2lem1  27796  wallispi2lem2  27797  wallispi2  27798  stirlinglem1  27799  stirlinglem2  27800  stirlinglem3  27801  stirlinglem4  27802  stirlinglem5  27803  stirlinglem7  27805  stirlinglem8  27806  stirlinglem10  27808  stirlinglem11  27809  stirlinglem12  27810  stirlinglem13  27811  stirlinglem14  27812  stirlinglem15  27813  cdleme31fv2  31190  tendopl2  31574  tendoi2  31592  erngplus2  31601  erngplus2-rN  31609  hlhilset  32735
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-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-mpt 4268  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-iota 5418  df-fun 5456  df-fv 5462
  Copyright terms: Public domain W3C validator