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

Theorem fvmptd 5961
Description: Deduction version of fvmpt 5956. (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 5874 . 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 3457 . . . 4  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
6 fvmptd.4 . . . 4  |-  ( ph  ->  C  e.  V )
75, 6eqeltrd 2545 . . 3  |-  ( ph  ->  [_ A  /  x ]_ B  e.  V
)
8 eqid 2457 . . . 4  |-  ( x  e.  D  |->  B )  =  ( x  e.  D  |->  B )
98fvmpts 5958 . . 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 2502 1  |-  ( ph  ->  ( F `  A
)  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395    e. wcel 1819   [_csb 3430    |-> cmpt 4515   ` cfv 5594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-iota 5557  df-fun 5596  df-fv 5602
This theorem is referenced by:  fvmptdv2  5970  mpt2curryvald  7017  ttukeylem3  8908  ccatval1  12604  ccatval2  12605  repswsymb  12758  prdsvscafval  14897  mrcval  15027  cidval  15094  isofval  15173  isofn  15191  cicfval  15213  subcid  15263  idfu2nd  15293  resf2nd  15311  fuccoval  15379  fucid  15387  initoval  15403  termoval  15404  zerooval  15405  homaval  15437  idaval  15464  setcval  15483  setcid  15492  catcval  15502  catcid  15509  estrcval  15520  estrcid  15530  funcestrcsetclem1  15536  funcsetcestrclem1  15550  prf1  15596  prf2  15598  curf1  15621  curf11  15622  curf2val  15626  hofval  15648  hof2  15653  yonval  15657  yonedalem4a  15671  frmdval  16146  vrmdval  16152  pmtrdifwrdellem3  16635  gexval  16725  pj1val  16840  dpjval  17232  sraval  17949  opsrval  18266  cply1mul  18462  cply1coe0  18468  cply1coe0bi  18469  gsummoncoe1  18473  evls1sca  18487  frlmphl  18939  mat1rhmval  19108  scmatrhmval  19156  mvmulfv  19173  mavmulfv  19175  mdetuni0  19250  mat2pmatval  19352  m2cpm  19369  cpm2mval  19378  m2cpminvid2lem  19382  decpmatid  19398  decpmatmullem  19399  pmatcollpw2lem  19405  monmatcollpw  19407  pmatcollpw3fi1lem1  19414  pm2mpfval  19424  mply1topmatval  19432  mp2pm2mplem1  19434  mp2pm2mplem4  19437  pm2mpmhmlem2  19447  chpmatval  19459  chfacfscmul0  19486  chfacfscmulgsum  19488  chfacfpmmul0  19490  chfacfpmmulgsum  19492  lmfval  19860  kgenval  20162  ptval  20197  fcfval  20660  cnextfval  20688  ustval  20831  utopval  20861  ustuqtoplem  20868  utopsnneiplem  20876  tusval  20895  blfvalps  21012  tmsval  21110  metuvalOLD  21178  metuval  21179  caufval  21840  rrxmvallem  21957  rrxmval  21958  taylpval  22888  efgh  23054  logexprlim  23626  dchrval  23635  dchr1  23658  mirval  24162  mirfv  24163  israg  24200  perpln1  24213  perpln2  24214  isperp  24215  ishpg  24254  midf  24268  ismidb  24270  lmif  24277  islmib  24279  edgval  24466  wlkiswwlk2lem2  24819  clwlkisclwwlklem2fv1  24909  clwlkisclwwlklem2fv2  24910  sgnsval  27878  metidval  28030  pstmval  28035  qqhvval  28125  indv  28187  indval  28188  indfval  28191  esummulc1  28253  esumcvg  28258  ofcval  28271  sigagenval  28313  measinb  28365  omsval  28437  omsfval  28438  omssubadd  28444  carsgval  28447  sitgfval  28480  eulerpartlemsv1  28492  eulerpartlems  28496  eulerpartlemgvv  28512  fibp1  28537  totprobd  28562  probmeasb  28566  cndprobval  28569  dstrvprob  28607  dstfrvinc  28612  dstfrvclim1  28613  ballotlemfval  28625  ballotlemsv  28645  gsumnunsn  28690  signsply0  28705  signstfval  28718  afsval  28748  lgamgulmlem2  28769  lgamcvglem  28779  cvmliftlem9  28935  mvrsval  29062  mrsubfval  29065  mrsubval  29066  msubfval  29081  msubval  29082  msrval  29095  relexp1g  29253  rtrclreclem.subset  29286  rtrclreclem.min  29288  dfrtrcl2  29289  mblfinlem2  30257  areacirc  30317  itgpowd  31386  dvgrat  31397  radcnvrat  31399  hashnzfzclim  31431  binomcxplemnn0  31458  binomcxplemrat  31459  binomcxplemfrat  31460  binomcxplemradcnv  31461  binomcxplemcvg  31463  binomcxplemdvsum  31464  binomcxplemnotnn0  31465  fmuldfeqlem1  31779  clim1fr1  31810  climrec  31812  climexp  31814  climneg  31819  mullimcf  31832  divcnvg  31836  sumnnodd  31839  expfac  31866  cncfshift  31879  icccncfext  31893  cncfioobdlem  31902  dvsinax  31911  fperdvper  31918  dvcosax  31926  ioodvbdlimc1lem1  31931  ioodvbdlimc1lem2  31932  ioodvbdlimc2lem  31934  dvnmul  31943  dvnprodlem1  31946  dvnprodlem2  31947  dvnprodlem3  31948  itgsinexp  31956  itgcoscmulx  31971  itgsincmulx  31976  itgsubsticclem  31977  itgsubsticc  31978  itgiccshift  31982  stoweidlem7  31992  stoweidlem17  32002  stoweidlem32  32017  stoweidlem34  32019  wallispilem4  32053  wallispilem5  32054  wallispi  32055  wallispi2lem1  32056  wallispi2lem2  32057  wallispi2  32058  stirlinglem1  32059  stirlinglem2  32060  stirlinglem3  32061  stirlinglem4  32062  stirlinglem5  32063  stirlinglem7  32065  stirlinglem8  32066  stirlinglem10  32068  stirlinglem11  32069  stirlinglem12  32070  stirlinglem13  32071  stirlinglem14  32072  stirlinglem15  32073  dirkerval2  32079  dirkercncflem2  32089  fourierdlem7  32099  fourierdlem13  32105  fourierdlem14  32106  fourierdlem16  32108  fourierdlem18  32110  fourierdlem19  32111  fourierdlem21  32113  fourierdlem22  32114  fourierdlem26  32118  fourierdlem37  32129  fourierdlem39  32131  fourierdlem41  32133  fourierdlem48  32140  fourierdlem49  32141  fourierdlem50  32142  fourierdlem51  32143  fourierdlem53  32145  fourierdlem62  32154  fourierdlem63  32155  fourierdlem65  32157  fourierdlem73  32165  fourierdlem74  32166  fourierdlem75  32167  fourierdlem76  32168  fourierdlem79  32171  fourierdlem81  32173  fourierdlem82  32174  fourierdlem83  32175  fourierdlem84  32176  fourierdlem88  32180  fourierdlem89  32181  fourierdlem90  32182  fourierdlem91  32183  fourierdlem92  32184  fourierdlem93  32185  fourierdlem97  32189  fourierdlem101  32193  fourierdlem103  32195  fourierdlem104  32196  fourierdlem111  32203  fourierdlem112  32204  fouriersw  32217  elaa2lem  32219  etransclem1  32221  etransclem12  32232  etransclem13  32233  etransclem17  32237  etransclem18  32238  etransclem21  32241  etransclem27  32247  etransclem31  32251  etransclem32  32252  etransclem33  32253  etransclem35  32255  etransclem46  32266  etransclem48  32268  vtxval  32645  gordval  32650  gsizval  32651  clintopval  32790  assintopval  32791  c0mgm  32859  c0mhm  32860  c0snmgmhm  32864  c0snmhm  32865  zrrnghm  32867  rngcvalOLD  32913  rngcval  32914  rngcidOLD  32943  zrinitorngc  32952  zrtermorngc  32953  ringcvalOLD  32959  ringcval  32960  funcringcsetcOLD2lem1  32988  ringcidOLD  33006  funcringcsetclem1OLD  33011  zrtermoringc  33022  rhmsubcOLDlem3  33059  scmsuppss  33109  ply1mulgsum  33134  lincop  33153  lincext3  33201  lindslinindsimp1  33202  lindsrng01  33213  lincresunit2  33223  lincresunit3lem1  33224  islindeps2  33228  bj-finsumval0  34806  cdleme31fv2  36262  tendopl2  36646  tendoi2  36664  erngplus2  36673  erngplus2-rN  36681  hlhilset  37807
  Copyright terms: Public domain W3C validator