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

Theorem fvmptd 5800
Description: Deduction version of fvmpt 5795. (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 5714 . 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 3335 . . . 4  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
6 fvmptd.4 . . . 4  |-  ( ph  ->  C  e.  V )
75, 6eqeltrd 2517 . . 3  |-  ( ph  ->  [_ A  /  x ]_ B  e.  V
)
8 eqid 2443 . . . 4  |-  ( x  e.  D  |->  B )  =  ( x  e.  D  |->  B )
98fvmpts 5797 . . 3  |-  ( ( A  e.  D  /\  [_ A  /  x ]_ B  e.  V )  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
103, 7, 9syl2anc 661 . 2  |-  ( ph  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
112, 10, 53eqtrd 2479 1  |-  ( ph  ->  ( F `  A
)  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   [_csb 3309    e. cmpt 4371   ` cfv 5439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-iota 5402  df-fun 5441  df-fv 5447
This theorem is referenced by:  fvmptdv2  5808  mpt2curryvald  6810  ttukeylem3  8701  ccatval1  12297  ccatval2  12298  repswsymb  12433  prdsvscafval  14439  mrcval  14569  cidval  14636  subcid  14778  idfu2nd  14808  resf2nd  14826  fuccoval  14894  fucid  14902  homaval  14920  idaval  14947  setcval  14966  setcid  14975  catcval  14985  catcid  14992  prf1  15031  prf2  15033  curf1  15056  curf11  15057  curf2val  15061  hofval  15083  hof2  15088  yonval  15092  yonedalem4a  15106  frmdval  15550  vrmdval  15556  pmtrdifwrdellem3  16010  gexval  16098  pj1val  16213  dpjval  16577  sraval  17279  opsrval  17578  evls1sca  17780  frlmphl  18228  mvmulfv  18377  mavmulfv  18379  mdetuni0  18449  lmfval  18858  kgenval  19130  ptval  19165  fcfval  19628  cnextfval  19656  ustval  19799  utopval  19829  ustuqtoplem  19836  utopsnneiplem  19844  tusval  19863  blfvalps  19980  tmsval  20078  metuvalOLD  20146  metuval  20147  caufval  20808  rrxmvallem  20925  rrxmval  20926  taylpval  21854  logexprlim  22586  dchrval  22595  dchr1  22618  mirval  23081  mirfv  23082  israg  23113  isperp  23125  sgnsval  26213  metidval  26339  pstmval  26344  qqhvval  26434  indv  26491  indval  26492  indfval  26495  esummulc1  26552  esumcvg  26557  ofcval  26563  sigagenval  26605  measinb  26657  omsval  26730  omsfval  26731  sitgfval  26749  eulerpartlemsv1  26761  eulerpartlems  26765  eulerpartlemgvv  26781  fibp1  26806  totprobd  26831  probmeasb  26835  cndprobval  26838  dstrvprob  26876  dstfrvinc  26881  dstfrvclim1  26882  ballotlemfval  26894  ballotlemsv  26914  gsumnunsn  26959  signsply0  26974  signstfval  26987  afsval  27017  lgamgulmlem2  27038  lgamcvglem  27048  cvmliftlem9  27204  relexp0  27353  relexpsucr  27354  rtrclreclem.subset  27369  rtrclreclem.min  27371  dfrtrcl2  27372  mblfinlem2  28455  areacirc  28515  itgpowd  29616  fmuldfeqlem1  29789  clim1fr1  29800  climrec  29802  climexp  29804  climneg  29809  itgsinexp  29821  stoweidlem7  29828  stoweidlem17  29838  stoweidlem32  29853  stoweidlem34  29855  wallispilem4  29889  wallispilem5  29890  wallispi  29891  wallispi2lem1  29892  wallispi2lem2  29893  wallispi2  29894  stirlinglem1  29895  stirlinglem2  29896  stirlinglem3  29897  stirlinglem4  29898  stirlinglem5  29899  stirlinglem7  29901  stirlinglem8  29902  stirlinglem10  29904  stirlinglem11  29905  stirlinglem12  29906  stirlinglem13  29907  stirlinglem14  29908  stirlinglem15  29909  wlkiswwlk2lem2  30352  clwlkisclwwlklem2fv1  30470  clwlkisclwwlklem2fv2  30471  scmsuppss  30815  gsummoncoe1  30876  ply1mulgsum  30881  cply1coe0  30882  cply1coe0bi  30883  cply1mul  30884  lincop  30939  lincext3  30987  lindslinindsimp1  30988  lindsrng01  30999  lincresunit2  31009  lincresunit3lem1  31010  islindeps2  31014  mat2pmatval  31075  mat2cnstpmat  31092  m2pminvval  31098  m2pminv2lem  31100  mply1topmatval  31109  pmatcollpw1id  31114  pmatcollpw1dstlem1  31115  pmatcollpw2lem  31120  pmattomply1  31126  mp2pm2mplem1  31131  mp2pm2mplem4  31134  pmattomply1mhmlem2  31144  bj-finsumval0  32679  cdleme31fv2  34133  tendopl2  34517  tendoi2  34535  erngplus2  34544  erngplus2-rN  34552  hlhilset  35678
  Copyright terms: Public domain W3C validator