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

Theorem fvmptd 5982
Description: Deduction version of fvmpt 5976. (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 5894 . 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 3402 . . . 4  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
6 fvmptd.4 . . . 4  |-  ( ph  ->  C  e.  V )
75, 6eqeltrd 2540 . . 3  |-  ( ph  ->  [_ A  /  x ]_ B  e.  V
)
8 eqid 2462 . . . 4  |-  ( x  e.  D  |->  B )  =  ( x  e.  D  |->  B )
98fvmpts 5979 . . 3  |-  ( ( A  e.  D  /\  [_ A  /  x ]_ B  e.  V )  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
103, 7, 9syl2anc 671 . 2  |-  ( ph  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
112, 10, 53eqtrd 2500 1  |-  ( ph  ->  ( F `  A
)  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455    e. wcel 1898   [_csb 3375    |-> cmpt 4477   ` cfv 5605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-iota 5569  df-fun 5607  df-fv 5613
This theorem is referenced by:  fvmptdv2  5991  fvmptopab1  6364  bropfvvvv  6908  mpt2curryvald  7048  ttukeylem3  8972  ccatval1  12764  ccatval2  12765  repswsymb  12920  relexp1g  13144  rtrclreclem2  13177  rtrclreclem4  13179  dfrtrcl2  13180  lcmslefacOLD  14641  lcmfval  14646  lcmf0val  14647  lcmfvalOLD  14650  prmoval  15046  fvprmselelfz  15057  fvprmselgcd1  15058  prmodvdslcmf  15060  prmgaplcmlem1OLD  15067  prmormapnnOLD  15069  prmdvdsprmorOLD  15070  prmorlefacOLD  15073  prmorlelcmsOLDOLD  15077  prmgap  15084  prmgaplcm  15086  prmgapprmo  15088  prdsvscafval  15433  mrcval  15571  cidval  15638  isofval  15717  isofn  15735  cicfval  15757  subcid  15807  idfu2nd  15837  resf2nd  15855  fuccoval  15923  fucid  15931  initoval  15947  termoval  15948  zerooval  15949  homaval  15981  idaval  16008  setcval  16027  setcid  16036  catcval  16046  catcid  16053  estrcval  16064  estrcid  16074  funcestrcsetclem1  16080  funcsetcestrclem1  16094  prf1  16140  prf2  16142  curf1  16165  curf11  16166  curf2val  16170  hofval  16192  hof2  16197  yonval  16201  yonedalem4a  16215  frmdval  16690  vrmdval  16696  pmtrdifwrdellem3  17179  gexval  17282  gexvalOLD  17284  pj1val  17400  dpjval  17744  sraval  18454  opsrval  18753  cply1mul  18942  cply1coe0  18948  cply1coe0bi  18949  gsummoncoe1  18953  evls1sca  18967  frlmphl  19394  mat1rhmval  19559  scmatrhmval  19607  mvmulfv  19624  mavmulfv  19626  mdetuni0  19701  mat2pmatval  19803  m2cpm  19820  cpm2mval  19829  m2cpminvid2lem  19833  decpmatid  19849  decpmatmullem  19850  pmatcollpw2lem  19856  monmatcollpw  19858  pmatcollpw3fi1lem1  19865  pm2mpfval  19875  mply1topmatval  19883  mp2pm2mplem1  19885  mp2pm2mplem4  19888  pm2mpmhmlem2  19898  chpmatval  19910  chfacfscmul0  19937  chfacfscmulgsum  19939  chfacfpmmul0  19941  chfacfpmmulgsum  19943  lmfval  20303  kgenval  20605  ptval  20640  fcfval  21103  cnextfval  21132  ustval  21272  utopval  21302  ustuqtoplem  21309  utopsnneiplem  21317  tusval  21336  blfvalps  21453  tmsval  21551  metuval  21619  caufval  22300  rrxmvallem  22413  rrxmval  22414  taylpval  23378  efgh  23546  lgamgulmlem2  24011  lgamcvglem  24021  logexprlim  24209  dchrval  24218  dchr1  24241  ishlg  24703  mirval  24756  mirfv  24757  israg  24798  perpln1  24811  perpln2  24812  isperp  24813  ishpg  24857  midf  24874  ismidb  24876  lmif  24883  islmib  24885  edgval  25122  wlkiswwlk2lem2  25476  clwlkisclwwlklem2fv1  25566  clwlkisclwwlklem2fv2  25567  sgnsval  28542  psgnfzto1stlem  28664  fzto1stfv1  28665  madjusmdetlem2  28705  metidval  28744  pstmval  28749  qqhvval  28838  indv  28885  indval  28886  indfval  28889  esummulc1  28953  esumcvg  28958  ofcval  28971  sigagenval  29013  measinb  29094  omsval  29167  omsfval  29168  omsvalOLD  29171  omsfvalOLD  29172  omssubadd  29178  omssubaddOLD  29182  carsgval  29185  sitgfval  29224  eulerpartlemsv1  29239  eulerpartlems  29243  eulerpartlemgvv  29259  fibp1  29284  totprobd  29309  probmeasb  29313  cndprobval  29316  dstrvprob  29354  dstfrvinc  29359  dstfrvclim1  29360  ballotlemfval  29372  ballotlemsv  29392  ballotlemsvOLD  29430  gsumnunsn  29475  signsply0  29490  signstfval  29503  afsval  29538  cvmliftlem9  30066  mvrsval  30193  mrsubfval  30196  mrsubval  30197  msubfval  30212  msubval  30213  msrval  30226  fwddifval  30979  fwddifnval  30980  bj-finsumval0  31748  poimirlem1  31987  poimirlem2  31988  poimirlem5  31991  poimirlem6  31992  poimirlem7  31993  poimirlem10  31996  poimirlem11  31997  poimirlem12  31998  poimirlem19  32005  poimirlem22  32008  mblfinlem2  32024  areacirc  32083  cdleme31fv2  34006  tendopl2  34390  tendoi2  34408  erngplus2  34417  erngplus2-rN  34425  hlhilset  35551  itgpowd  36145  iunrelexpmin1  36346  iunrelexpmin2  36350  dvgrat  36706  radcnvrat  36708  hashnzfzclim  36716  binomcxplemnn0  36743  binomcxplemrat  36744  binomcxplemfrat  36745  binomcxplemradcnv  36746  binomcxplemcvg  36748  binomcxplemdvsum  36749  binomcxplemnotnn0  36750  projf1o  37528  mapss2  37540  fmuldfeqlem1  37746  clim1fr1  37765  climrec  37767  climexp  37769  climneg  37775  mullimcf  37789  divcnvg  37793  sumnnodd  37796  expfac  37824  cncfshift  37837  icccncfext  37851  cncfioobdlem  37860  dvsinax  37869  fperdvper  37876  dvcosax  37884  ioodvbdlimc1lem1  37889  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem1OLD  37891  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  dvnmul  37904  dvnprodlem1  37907  dvnprodlem2  37908  dvnprodlem3  37909  itgsinexp  37917  itgcoscmulx  37932  itgsincmulx  37937  itgsubsticclem  37938  itgsubsticc  37939  itgiccshift  37943  stoweidlem7  37968  stoweidlem17  37978  stoweidlem32  37994  stoweidlem34  37996  wallispilem4  38031  wallispilem5  38032  wallispi  38033  wallispi2lem1  38034  wallispi2lem2  38035  wallispi2  38036  stirlinglem1  38037  stirlinglem2  38038  stirlinglem3  38039  stirlinglem4  38040  stirlinglem5  38041  stirlinglem7  38043  stirlinglem8  38044  stirlinglem10  38046  stirlinglem11  38047  stirlinglem12  38048  stirlinglem13  38049  stirlinglem14  38050  stirlinglem15  38051  dirkerval2  38057  dirkercncflem2  38067  fourierdlem7  38077  fourierdlem13  38083  fourierdlem14  38084  fourierdlem16  38086  fourierdlem18  38088  fourierdlem19  38089  fourierdlem21  38091  fourierdlem22  38092  fourierdlem26  38096  fourierdlem37  38108  fourierdlem39  38110  fourierdlem41  38112  fourierdlem48  38119  fourierdlem49  38120  fourierdlem50  38121  fourierdlem51  38122  fourierdlem53  38124  fourierdlem62  38133  fourierdlem63  38134  fourierdlem65  38136  fourierdlem73  38144  fourierdlem74  38145  fourierdlem75  38146  fourierdlem76  38147  fourierdlem79  38150  fourierdlem81  38152  fourierdlem82  38153  fourierdlem83  38154  fourierdlem84  38155  fourierdlem88  38159  fourierdlem89  38160  fourierdlem90  38161  fourierdlem91  38162  fourierdlem92  38163  fourierdlem93  38164  fourierdlem97  38168  fourierdlem101  38172  fourierdlem103  38174  fourierdlem104  38175  fourierdlem111  38182  fourierdlem112  38183  fouriersw  38196  elaa2lem  38198  elaa2lemOLD  38199  etransclem1  38201  etransclem12  38212  etransclem13  38213  etransclem17  38217  etransclem18  38218  etransclem21  38221  etransclem27  38227  etransclem31  38231  etransclem32  38232  etransclem33  38233  etransclem35  38235  etransclem46  38246  etransclem48OLD  38248  etransclem48  38249  rrxtopnfi  38256  salgenval  38283  sge0val  38311  sge0z  38320  sge0snmpt  38328  sge0xp  38374  nnfoctbdjlem  38398  psmeasurelem  38413  psmeasure  38414  omeiunltfirp  38448  carageniuncllem1  38450  carageniuncllem2  38451  caratheodorylem1  38455  0ome  38458  vonval  38469  ovnval  38470  ovnval2  38474  hoicvr  38477  ovnval2b  38481  hoiprodcl2  38484  ovnlecvr  38487  ovncvrrp  38493  ovn0lem  38494  ovnsubaddlem1  38499  hsphoif  38505  hoidmvval  38506  hsphoival  38508  hoidmv1le  38523  hoidmvlelem3  38526  ovnhoilem1  38530  ovnhoilem2  38531  hoidifhspval  38537  hspval  38538  ovncvr2  38540  hoidifhspval2  38544  hoidifhspval3  38548  hspmbllem2  38556  ovnsubadd2lem  38574  iccpval  38864  mptmpt2opabbrd  39172  edgaval  39356  uvtxaval  39605  vtxdgfval  39674  1wlksfval  39770  wlksfval  39771  vtxvalaltv  40064  gordval  40069  gsizval  40070  clintopval  40209  assintopval  40210  c0mgm  40278  c0mhm  40279  c0snmgmhm  40283  c0snmhm  40284  zrrnghm  40286  rngcvalALTV  40332  rngcval  40333  rngcidALTV  40362  zrinitorngc  40371  zrtermorngc  40372  ringcvalALTV  40378  ringcval  40379  funcringcsetcALTV2lem1  40407  ringcidALTV  40425  funcringcsetclem1ALTV  40430  zrtermoringc  40441  rhmsubcALTVlem3  40478  scmsuppss  40526  ply1mulgsum  40551  lincop  40570  lincext3  40618  lindslinindsimp1  40619  lindsrng01  40630  lincresunit2  40640  lincresunit3lem1  40641  islindeps2  40645  fdivmptfv  40725  refdivmptfv  40726  bigoval  40729  blenval  40751  digfval  40777
  Copyright terms: Public domain W3C validator