Theorem fvmptd 6197

Description: Deduction version of fvmpt 6191. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
fvmptd.1	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))
fvmptd.2	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
fvmptd.3	⊢ (𝜑 → 𝐴 ∈ 𝐷)
fvmptd.4	⊢ (𝜑 → 𝐶 ∈ 𝑉)

Assertion

Ref	Expression
fvmptd	⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷   𝜑,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptd

Step	Hyp	Ref	Expression
1		fvmptd.1	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))
2	1	fveq1d 6105	. 2 ⊢ (𝜑 → (𝐹‘𝐴) = ((𝑥 ∈ 𝐷 ↦ 𝐵)‘𝐴))
3		fvmptd.3	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
4		fvmptd.2	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
5	3, 4	csbied 3526	. . . 4 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
6		fvmptd.4	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
7	5, 6	eqeltrd 2688	. . 3 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉)
8		eqid 2610	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = (𝑥 ∈ 𝐷 ↦ 𝐵)
9	8	fvmpts 6194	. . 3 ⊢ ((𝐴 ∈ 𝐷 ∧ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐷 ↦ 𝐵)‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵)
10	3, 7, 9	syl2anc 691	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐵)‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵)
11	2, 10, 5	3eqtrd 2648	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ⦋csb 3499   ↦ cmpt 4643  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812

This theorem is referenced by:  fvmptdv2  6206  fvmptopab1  6594  bropfvvvv  7144  mpt2curryvald  7283  ttukeylem3  9216  ccatval1  13214  ccatval2  13215  repswsymb  13372  relexp1g  13614  rtrclreclem2  13647  rtrclreclem4  13649  dfrtrcl2  13650  lcmfval  15172  lcmf0val  15173  prmoval  15575  fvprmselelfz  15586  fvprmselgcd1  15587  prmodvdslcmf  15589  prmgap  15601  prmgaplcm  15602  prmgapprmo  15604  prdsvscafval  15963  mrcval  16093  cidval  16161  isofval  16240  isofn  16258  cicfval  16280  subcid  16330  idfu2nd  16360  resf2nd  16378  fuccoval  16446  fucid  16454  initoval  16470  termoval  16471  zerooval  16472  homaval  16504  idaval  16531  setcval  16550  setcid  16559  catcval  16569  catcid  16576  estrcval  16587  estrcid  16597  funcestrcsetclem1  16603  funcsetcestrclem1  16617  prf1  16663  prf2  16665  curf1  16688  curf11  16689  curf2val  16693  hofval  16715  hof2  16720  yonval  16724  yonedalem4a  16738  frmdval  17211  vrmdval  17217  pmtrdifwrdellem3  17726  gexval  17816  pj1val  17931  dpjval  18278  sraval  18997  opsrval  19295  cply1mul  19485  cply1coe0  19490  cply1coe0bi  19491  gsummoncoe1  19495  evls1sca  19509  frlmphl  19939  mat1rhmval  20104  scmatrhmval  20152  mvmulfv  20169  mavmulfv  20171  mdetuni0  20246  mat2pmatval  20348  m2cpm  20365  cpm2mval  20374  m2cpminvid2lem  20378  decpmatid  20394  decpmatmullem  20395  pmatcollpw2lem  20401  monmatcollpw  20403  pmatcollpw3fi1lem1  20410  pm2mpfval  20420  mply1topmatval  20428  mp2pm2mplem1  20430  mp2pm2mplem4  20433  pm2mpmhmlem2  20443  chpmatval  20455  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulgsum  20488  lmfval  20846  kgenval  21148  ptval  21183  fcfval  21647  cnextfval  21676  ustval  21816  utopval  21846  ustuqtoplem  21853  utopsnneiplem  21861  tusval  21880  blfvalps  21998  tmsval  22096  metuval  22164  caufval  22881  rrxmvallem  22995  rrxmval  22996  taylpval  23925  efgh  24091  lgamgulmlem2  24556  lgamcvglem  24566  logexprlim  24750  dchrval  24759  dchr1  24782  gausslemma2dlem2  24892  gausslemma2dlem3  24893  gausslemma2dlem4  24894  2lgslem1b  24917  ishlg  25297  mirval  25350  mirfv  25351  israg  25392  perpln1  25405  perpln2  25406  isperp  25407  ishpg  25451  midf  25468  ismidb  25470  lmif  25477  islmib  25479  edgaval  25794  edgval  25868  wlkiswwlk2lem2  26220  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2fv2  26311  sgnsval  29059  psgnfzto1stlem  29181  fzto1stfv1  29182  madjusmdetlem2  29222  metidval  29261  pstmval  29266  qqhvval  29355  indv  29402  indval  29403  indfval  29406  esummulc1  29470  esumcvg  29475  ofcval  29488  sigagenval  29530  measinb  29611  omsval  29682  omsfval  29683  omssubadd  29689  carsgval  29692  sitgfval  29730  eulerpartlemsv1  29745  eulerpartlems  29749  eulerpartlemgvv  29765  fibp1  29790  totprobd  29815  probmeasb  29819  cndprobval  29822  dstrvprob  29860  dstfrvinc  29865  dstfrvclim1  29866  ballotlemfval  29878  ballotlemsv  29898  gsumnunsn  29942  signsply0  29954  signstfval  29967  afsval  30002  cvmliftlem9  30529  mvrsval  30656  mrsubfval  30659  mrsubval  30660  msubfval  30675  msubval  30676  msrval  30689  fwddifval  31439  fwddifnval  31440  knoppcnlem1  31653  knoppcnlem4  31656  knoppcnlem6  31658  knoppcnlem7  31659  knoppcnlem9  31661  unbdqndv2lem2  31671  knoppndvlem4  31676  knoppndvlem6  31678  bj-finsumval0  32324  poimirlem1  32580  poimirlem2  32581  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem19  32598  poimirlem22  32601  mblfinlem2  32617  areacirc  32675  cdleme31fv2  34699  tendopl2  35083  tendoi2  35101  erngplus2  35110  erngplus2-rN  35118  hlhilset  36244  itgpowd  36819  iunrelexpmin1  37019  iunrelexpmin2  37023  rfovfvd  37316  rfovfvfvd  37317  rfovcnvf1od  37318  rfovcnvfvd  37321  fsovfvd  37324  fsovfvfvd  37325  fsovcnvlem  37327  dssmapfvd  37331  dssmapfv2d  37332  dssmapfv3d  37333  dssmapnvod  37334  clsk3nimkb  37358  dvgrat  37533  radcnvrat  37535  hashnzfzclim  37543  binomcxplemnn0  37570  binomcxplemrat  37571  binomcxplemfrat  37572  binomcxplemradcnv  37573  binomcxplemcvg  37575  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  projf1o  38381  mapss2  38392  fmuldfeqlem1  38649  clim1fr1  38668  climrec  38670  climexp  38672  climneg  38677  mullimcf  38690  divcnvg  38694  sumnnodd  38697  expfac  38724  fnlimfv  38730  fnlimabslt  38746  cncfshift  38759  icccncfext  38773  cncfioobdlem  38782  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvsinax  38801  fperdvper  38808  dvcosax  38816  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  itgsinexp  38846  itgcoscmulx  38861  itgsincmulx  38866  itgsubsticclem  38867  itgsubsticc  38868  itgiccshift  38872  stoweidlem7  38900  stoweidlem17  38910  stoweidlem32  38925  stoweidlem34  38927  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  wallispi2  38966  stirlinglem1  38967  stirlinglem2  38968  stirlinglem3  38969  stirlinglem4  38970  stirlinglem5  38971  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  dirkerval2  38987  dirkercncflem2  38997  fourierdlem7  39007  fourierdlem13  39013  fourierdlem14  39014  fourierdlem16  39016  fourierdlem18  39018  fourierdlem19  39019  fourierdlem21  39021  fourierdlem22  39022  fourierdlem26  39026  fourierdlem37  39037  fourierdlem39  39039  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem53  39052  fourierdlem62  39061  fourierdlem63  39062  fourierdlem65  39064  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem83  39082  fourierdlem84  39083  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem93  39092  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fouriersw  39124  elaa2lem  39126  etransclem1  39128  etransclem12  39139  etransclem13  39140  etransclem17  39144  etransclem18  39145  etransclem21  39148  etransclem27  39154  etransclem31  39158  etransclem32  39159  etransclem33  39160  etransclem35  39162  etransclem46  39173  etransclem48  39175  rrxtopnfi  39182  salgenval  39217  sge0val  39259  sge0z  39268  sge0snmpt  39276  sge0xp  39322  nnfoctbdjlem  39348  psmeasurelem  39363  psmeasure  39364  meaiuninclem  39373  meaiininclem  39376  omeiunltfirp  39409  carageniuncllem1  39411  carageniuncllem2  39412  caratheodorylem1  39416  0ome  39419  vonval  39430  ovnval  39431  ovnval2  39435  hoicvr  39438  ovnval2b  39442  hoiprodcl2  39445  ovnlecvr  39448  ovncvrrp  39454  ovn0lem  39455  ovnsubaddlem1  39460  hsphoif  39466  hoidmvval  39467  hsphoival  39469  hoidmv1le  39484  hoidmvlelem3  39487  ovnhoilem1  39491  ovnhoilem2  39492  hoidifhspval  39498  hspval  39499  ovncvr2  39501  hoidifhspval2  39505  hoidifhspval3  39509  hspmbllem2  39517  ovnsubadd2lem  39535  vonioolem2  39572  vonicclem2  39575  issmflem  39613  smfid  39639  iccpval  39953  fmtno  39979  prmdvdsfmtnof1  40037  mptmpt2opabbrd  40335  uvtxaval  40613  vtxdgfval  40683  1wlksfval  40811  wlksfval  40812  crctcsh1wlkn0lem2  41014  crctcsh1wlkn0lem3  41015  crctcsh  41027  wwlks  41038  1wlkiswwlks2lem2  41067  1wlkpwwlkf1ouspgr  41076  clwwlks  41187  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2fv2  41205  2wspmdisj  41501  fusgreghash2wsp  41502  av-numclwlk1lem2fv  41523  av-numclwlk2lem2fv  41534  clintopval  41630  assintopval  41631  c0mgm  41699  c0mhm  41700  c0snmgmhm  41704  c0snmhm  41705  zrrnghm  41707  rngcvalALTV  41753  rngcval  41754  rngcidALTV  41783  zrinitorngc  41792  zrtermorngc  41793  ringcvalALTV  41799  ringcval  41800  funcringcsetcALTV2lem1  41828  ringcidALTV  41846  funcringcsetclem1ALTV  41851  zrtermoringc  41862  rhmsubcALTVlem3  41899  scmsuppss  41947  ply1mulgsum  41972  lincop  41991  lincext3  42039  lindslinindsimp1  42040  lindsrng01  42051  lincresunit2  42061  lincresunit3lem1  42062  islindeps2  42066  fdivmptfv  42137  refdivmptfv  42138  bigoval  42141  blenval  42163  digfval  42189  amgmwlem  42357