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

Theorem fvmptd 5970
Description: Deduction version of fvmpt 5964. (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 5883 . 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 3422 . . . 4  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
6 fvmptd.4 . . . 4  |-  ( ph  ->  C  e.  V )
75, 6eqeltrd 2507 . . 3  |-  ( ph  ->  [_ A  /  x ]_ B  e.  V
)
8 eqid 2422 . . . 4  |-  ( x  e.  D  |->  B )  =  ( x  e.  D  |->  B )
98fvmpts 5967 . . 3  |-  ( ( A  e.  D  /\  [_ A  /  x ]_ B  e.  V )  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
103, 7, 9syl2anc 665 . 2  |-  ( ph  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
112, 10, 53eqtrd 2467 1  |-  ( ph  ->  ( F `  A
)  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1872   [_csb 3395    |-> cmpt 4482   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-iota 5565  df-fun 5603  df-fv 5609
This theorem is referenced by:  fvmptdv2  5979  mpt2curryvald  7028  ttukeylem3  8948  ccatval1  12726  ccatval2  12727  repswsymb  12879  relexp1g  13089  rtrclreclem2  13122  rtrclreclem4  13124  dfrtrcl2  13125  lcmslefacOLD  14585  lcmfval  14590  lcmf0val  14591  lcmfvalOLD  14594  prmoval  14990  fvprmselelfz  15001  fvprmselgcd1  15002  prmodvdslcmf  15004  prmgaplcmlem1OLD  15011  prmormapnnOLD  15013  prmdvdsprmorOLD  15014  prmorlefacOLD  15017  prmorlelcmsOLDOLD  15021  prmgap  15028  prmgaplcm  15030  prmgapprmo  15032  prdsvscafval  15377  mrcval  15515  cidval  15582  isofval  15661  isofn  15679  cicfval  15701  subcid  15751  idfu2nd  15781  resf2nd  15799  fuccoval  15867  fucid  15875  initoval  15891  termoval  15892  zerooval  15893  homaval  15925  idaval  15952  setcval  15971  setcid  15980  catcval  15990  catcid  15997  estrcval  16008  estrcid  16018  funcestrcsetclem1  16024  funcsetcestrclem1  16038  prf1  16084  prf2  16086  curf1  16109  curf11  16110  curf2val  16114  hofval  16136  hof2  16141  yonval  16145  yonedalem4a  16159  frmdval  16634  vrmdval  16640  pmtrdifwrdellem3  17123  gexval  17226  gexvalOLD  17228  pj1val  17344  dpjval  17688  sraval  18398  opsrval  18697  cply1mul  18886  cply1coe0  18892  cply1coe0bi  18893  gsummoncoe1  18897  evls1sca  18911  frlmphl  19337  mat1rhmval  19502  scmatrhmval  19550  mvmulfv  19567  mavmulfv  19569  mdetuni0  19644  mat2pmatval  19746  m2cpm  19763  cpm2mval  19772  m2cpminvid2lem  19776  decpmatid  19792  decpmatmullem  19793  pmatcollpw2lem  19799  monmatcollpw  19801  pmatcollpw3fi1lem1  19808  pm2mpfval  19818  mply1topmatval  19826  mp2pm2mplem1  19828  mp2pm2mplem4  19831  pm2mpmhmlem2  19841  chpmatval  19853  chfacfscmul0  19880  chfacfscmulgsum  19882  chfacfpmmul0  19884  chfacfpmmulgsum  19886  lmfval  20246  kgenval  20548  ptval  20583  fcfval  21046  cnextfval  21075  ustval  21215  utopval  21245  ustuqtoplem  21252  utopsnneiplem  21260  tusval  21279  blfvalps  21396  tmsval  21494  metuval  21562  caufval  22243  rrxmvallem  22356  rrxmval  22357  taylpval  23320  efgh  23488  lgamgulmlem2  23953  lgamcvglem  23963  logexprlim  24151  dchrval  24160  dchr1  24183  ishlg  24645  mirval  24698  mirfv  24699  israg  24740  perpln1  24753  perpln2  24754  isperp  24755  ishpg  24799  midf  24816  ismidb  24818  lmif  24825  islmib  24827  edgval  25064  wlkiswwlk2lem2  25418  clwlkisclwwlklem2fv1  25508  clwlkisclwwlklem2fv2  25509  sgnsval  28498  psgnfzto1stlem  28621  fzto1stfv1  28622  madjusmdetlem2  28662  metidval  28701  pstmval  28706  qqhvval  28795  indv  28842  indval  28843  indfval  28846  esummulc1  28910  esumcvg  28915  ofcval  28928  sigagenval  28970  measinb  29051  omsval  29125  omsfval  29126  omsvalOLD  29129  omsfvalOLD  29130  omssubadd  29136  omssubaddOLD  29140  carsgval  29143  sitgfval  29182  eulerpartlemsv1  29197  eulerpartlems  29201  eulerpartlemgvv  29217  fibp1  29242  totprobd  29267  probmeasb  29271  cndprobval  29274  dstrvprob  29312  dstfrvinc  29317  dstfrvclim1  29318  ballotlemfval  29330  ballotlemsv  29350  ballotlemsvOLD  29388  gsumnunsn  29433  signsply0  29448  signstfval  29461  afsval  29496  cvmliftlem9  30024  mvrsval  30151  mrsubfval  30154  mrsubval  30155  msubfval  30170  msubval  30171  msrval  30184  fwddifval  30934  fwddifnval  30935  bj-finsumval0  31666  poimirlem1  31905  poimirlem2  31906  poimirlem5  31909  poimirlem6  31910  poimirlem7  31911  poimirlem10  31914  poimirlem11  31915  poimirlem12  31916  poimirlem19  31923  poimirlem22  31926  mblfinlem2  31942  areacirc  32001  cdleme31fv2  33929  tendopl2  34313  tendoi2  34331  erngplus2  34340  erngplus2-rN  34348  hlhilset  35474  itgpowd  36069  iunrelexpmin1  36270  iunrelexpmin2  36274  dvgrat  36631  radcnvrat  36633  hashnzfzclim  36641  binomcxplemnn0  36668  binomcxplemrat  36669  binomcxplemfrat  36670  binomcxplemradcnv  36671  binomcxplemcvg  36673  binomcxplemdvsum  36674  binomcxplemnotnn0  36675  projf1o  37435  fmuldfeqlem1  37600  clim1fr1  37619  climrec  37621  climexp  37623  climneg  37629  mullimcf  37643  divcnvg  37647  sumnnodd  37650  expfac  37678  cncfshift  37691  icccncfext  37705  cncfioobdlem  37714  dvsinax  37723  fperdvper  37730  dvcosax  37738  ioodvbdlimc1lem1  37743  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem1OLD  37745  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  dvnmul  37758  dvnprodlem1  37761  dvnprodlem2  37762  dvnprodlem3  37763  itgsinexp  37771  itgcoscmulx  37786  itgsincmulx  37791  itgsubsticclem  37792  itgsubsticc  37793  itgiccshift  37797  stoweidlem7  37807  stoweidlem17  37817  stoweidlem32  37833  stoweidlem34  37835  wallispilem4  37870  wallispilem5  37871  wallispi  37872  wallispi2lem1  37873  wallispi2lem2  37874  wallispi2  37875  stirlinglem1  37876  stirlinglem2  37877  stirlinglem3  37878  stirlinglem4  37879  stirlinglem5  37880  stirlinglem7  37882  stirlinglem8  37883  stirlinglem10  37885  stirlinglem11  37886  stirlinglem12  37887  stirlinglem13  37888  stirlinglem14  37889  stirlinglem15  37890  dirkerval2  37896  dirkercncflem2  37906  fourierdlem7  37916  fourierdlem13  37922  fourierdlem14  37923  fourierdlem16  37925  fourierdlem18  37927  fourierdlem19  37928  fourierdlem21  37930  fourierdlem22  37931  fourierdlem26  37935  fourierdlem37  37947  fourierdlem39  37949  fourierdlem41  37951  fourierdlem48  37958  fourierdlem49  37959  fourierdlem50  37960  fourierdlem51  37961  fourierdlem53  37963  fourierdlem62  37972  fourierdlem63  37973  fourierdlem65  37975  fourierdlem73  37983  fourierdlem74  37984  fourierdlem75  37985  fourierdlem76  37986  fourierdlem79  37989  fourierdlem81  37991  fourierdlem82  37992  fourierdlem83  37993  fourierdlem84  37994  fourierdlem88  37998  fourierdlem89  37999  fourierdlem90  38000  fourierdlem91  38001  fourierdlem92  38002  fourierdlem93  38003  fourierdlem97  38007  fourierdlem101  38011  fourierdlem103  38013  fourierdlem104  38014  fourierdlem111  38021  fourierdlem112  38022  fouriersw  38035  elaa2lem  38037  elaa2lemOLD  38038  etransclem1  38040  etransclem12  38051  etransclem13  38052  etransclem17  38056  etransclem18  38057  etransclem21  38060  etransclem27  38066  etransclem31  38070  etransclem32  38071  etransclem33  38072  etransclem35  38074  etransclem46  38085  etransclem48OLD  38087  etransclem48  38088  sge0val  38116  sge0z  38125  sge0snmpt  38133  sge0xp  38179  nnfoctbdjlem  38201  psmeasurelem  38216  psmeasure  38217  omeiunltfirp  38248  carageniuncllem1  38250  carageniuncllem2  38251  caratheodorylem1  38255  0ome  38258  vonval  38265  ovnval  38266  ovnval2  38271  hoicvr  38274  ovnval2b  38278  hoiprodcl2  38281  ovnlecvr  38284  ovncvrrp  38290  ovn0lem  38291  ovnsubaddlem1  38296  hsphoif  38302  hoidmvval  38303  hsphoival  38305  hoidmv1le  38320  hoidmvlelem3  38323  ovnhoilem1  38327  ovnhoilem2  38328  iccpval  38599  edgaval  39029  uvtxaval  39219  vtxvalaltv  39315  gordval  39320  gsizval  39321  clintopval  39460  assintopval  39461  c0mgm  39529  c0mhm  39530  c0snmgmhm  39534  c0snmhm  39535  zrrnghm  39537  rngcvalALTV  39583  rngcval  39584  rngcidALTV  39613  zrinitorngc  39622  zrtermorngc  39623  ringcvalALTV  39629  ringcval  39630  funcringcsetcALTV2lem1  39658  ringcidALTV  39676  funcringcsetclem1ALTV  39681  zrtermoringc  39692  rhmsubcALTVlem3  39729  scmsuppss  39779  ply1mulgsum  39804  lincop  39823  lincext3  39871  lindslinindsimp1  39872  lindsrng01  39883  lincresunit2  39893  lincresunit3lem1  39894  islindeps2  39898  fdivmptfv  39978  refdivmptfv  39979  bigoval  39982  blenval  40004  digfval  40030
  Copyright terms: Public domain W3C validator