Theorem fvmptd 6509

Description: Deduction version of fvmpt 6503. (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 6410	. 2 ⊢ (𝜑 → (𝐹‘𝐴) = ((𝑥 ∈ 𝐷 ↦ 𝐵)‘𝐴))
3		fvmptd.3	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
4		fvmptd.2	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
5	3, 4	csbied 3755	. . . 4 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
6		fvmptd.4	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
7	5, 6	eqeltrd 2885	. . 3 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉)
8		eqid 2806	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = (𝑥 ∈ 𝐷 ↦ 𝐵)
9	8	fvmpts 6506	. . 3 ⊢ ((𝐴 ∈ 𝐷 ∧ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐷 ↦ 𝐵)‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵)
10	3, 7, 9	syl2anc 575	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐵)‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵)
11	2, 10, 5	3eqtrd 2844	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637   ∈ wcel 2156  ⦋csb 3728   ↦ cmpt 4923  ‘cfv 6101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-iota 6064  df-fun 6103  df-fv 6109

This theorem is referenced by:  fvmptdv2  6519  fvmptopab  6927  mptmpt2opabbrd  7481  bropfvvvv  7491  mpt2curryvald  7631  djuss  9029  1stinl  9036  2ndinl  9037  1stinr  9038  2ndinr  9039  updjudhcoinlf  9041  updjudhcoinrg  9042  ttukeylem3  9618  ccatval1  13574  ccatval2  13575  repswsymb  13745  relexp1g  13989  rtrclreclem2  14022  rtrclreclem4  14024  dfrtrcl2  14025  lcmfval  15553  lcmf0val  15554  prmoval  15954  fvprmselelfz  15965  fvprmselgcd1  15966  prmodvdslcmf  15968  prmgap  15980  prmgaplcm  15981  prmgapprmo  15983  prdsvscafval  16345  mrcval  16475  cidval  16542  isofval  16621  isofn  16639  cicfval  16661  subcid  16711  idfu2nd  16741  resf2nd  16759  fuccoval  16827  fucid  16835  initoval  16851  termoval  16852  zerooval  16853  homaval  16885  idaval  16912  setcval  16931  setcid  16940  catcval  16950  catcid  16957  estrcval  16968  estrcid  16978  funcestrcsetclem1  16985  funcsetcestrclem1  16999  prf1  17045  prf2  17047  curf1  17070  curf11  17071  curf2val  17075  hofval  17097  hof2  17102  yonval  17106  yonedalem4a  17120  frmdval  17593  vrmdval  17599  pmtrdifwrdellem3  18104  gexval  18194  pj1val  18309  dpjval  18657  sraval  19385  opsrval  19683  cply1mul  19872  cply1coe0  19877  cply1coe0bi  19878  gsummoncoe1  19882  evls1sca  19896  frlmphl  20330  mat1rhmval  20496  scmatrhmval  20544  mvmulfv  20561  mavmulfv  20563  mdetuni0  20638  mat2pmatval  20742  m2cpm  20759  cpm2mval  20768  m2cpminvid2lem  20772  decpmatid  20788  decpmatmullem  20789  pmatcollpw2lem  20795  monmatcollpw  20797  pmatcollpw3fi1lem1  20804  pm2mpfval  20814  mply1topmatval  20822  mp2pm2mplem1  20824  mp2pm2mplem4  20827  pm2mpmhmlem2  20837  chpmatval  20849  chfacfscmul0  20876  chfacfscmulgsum  20878  chfacfpmmul0  20880  chfacfpmmulgsum  20882  lmfval  21250  kgenval  21552  ptval  21587  fcfval  22050  cnextfval  22079  ustval  22219  utopval  22249  ustuqtoplem  22256  utopsnneiplem  22264  tusval  22283  blfvalps  22401  tmsval  22499  metuval  22567  caufval  23285  rrxmvallem  23399  rrxmval  23400  taylpval  24335  efgh  24502  lgamgulmlem2  24970  lgamcvglem  24980  logexprlim  25164  dchrval  25173  dchr1  25196  gausslemma2dlem2  25306  gausslemma2dlem3  25307  gausslemma2dlem4  25308  2lgslem1b  25331  ishlg  25711  mirval  25764  mirfv  25765  israg  25806  perpln1  25819  perpln2  25820  isperp  25821  ishpg  25865  midf  25882  ismidb  25884  lmif  25891  islmib  25893  edgval  26155  edgvalOLD  26156  uvtxavalOLD  26506  vtxdgfval  26591  wksfval  26733  crctcshwlkn0lem2  26932  crctcshwlkn0lem3  26933  crctcsh  26945  wwlks  26956  wlkiswwlks2lem2  26997  wlkswwlksf1o  27006  clwwlk  27126  clwlkclwwlklem2fv1  27138  clwlkclwwlklem2fv2  27139  clwlkclwwlkf1  27153  numclwlk2lem2fv  27558  numclwlk2lem2fvOLD  27565  sgnsval  30053  psgnfzto1stlem  30175  fzto1stfv1  30176  madjusmdetlem2  30219  metidval  30258  pstmval  30263  qqhvval  30352  indv  30399  indval  30400  indfval  30403  esummulc1  30468  esumcvg  30473  ofcval  30486  sigagenval  30528  measinb  30609  omsval  30680  omsfval  30681  omssubadd  30687  carsgval  30690  sitgfval  30728  eulerpartlemsv1  30743  eulerpartlems  30747  eulerpartlemgvv  30763  fibp1  30788  totprobd  30813  probmeasb  30817  cndprobval  30820  dstrvprob  30858  dstfrvinc  30863  dstfrvclim1  30864  ballotlemfval  30876  ballotlemsv  30896  gsumnunsn  30940  signsply0  30953  signstfval  30966  fdvneggt  31003  fdvnegge  31005  itgexpif  31009  reprval  31013  breprexplema  31033  vtsval  31040  logdivsqrle  31053  hgt750lemg  31057  hgt750lemb  31059  afsval  31074  cvmliftlem9  31598  mvrsval  31725  mrsubfval  31728  mrsubval  31729  msubfval  31744  msubval  31745  msrval  31758  fwddifval  32590  fwddifnval  32591  knoppcnlem1  32800  knoppcnlem4  32803  knoppcnlem6  32805  knoppcnlem7  32806  knoppcnlem9  32808  unbdqndv2lem2  32818  knoppndvlem4  32823  knoppndvlem6  32825  bj-finsumval0  33464  poimirlem1  33723  poimirlem2  33724  poimirlem5  33727  poimirlem6  33728  poimirlem7  33729  poimirlem10  33732  poimirlem11  33733  poimirlem12  33734  poimirlem19  33741  poimirlem22  33744  mblfinlem2  33760  areacirc  33817  cdleme31fv2  36174  tendopl2  36558  tendoi2  36576  erngplus2  36585  erngplus2-rN  36593  hlhilset  37715  itgpowd  38300  iunrelexpmin1  38500  iunrelexpmin2  38504  rfovfvd  38796  rfovfvfvd  38797  rfovcnvf1od  38798  rfovcnvfvd  38801  fsovfvd  38804  fsovfvfvd  38805  fsovcnvlem  38807  dssmapfvd  38811  dssmapfv2d  38812  dssmapfv3d  38813  dssmapnvod  38814  clsk3nimkb  38838  dvgrat  39011  radcnvrat  39013  hashnzfzclim  39021  binomcxplemnn0  39048  binomcxplemrat  39049  binomcxplemfrat  39050  binomcxplemradcnv  39051  binomcxplemcvg  39053  binomcxplemdvsum  39054  binomcxplemnotnn0  39055  projf1o  39875  mapss2  39884  fvmptd2  39929  fmuldfeqlem1  40294  clim1fr1  40313  climrec  40315  climexp  40317  climneg  40322  mullimcf  40335  divcnvg  40339  sumnnodd  40342  expfac  40369  fnlimfv  40375  fnlimabslt  40391  supcnvlimsup  40452  icccncfext  40580  cncfioobdlem  40589  fprodsubrecnncnvlem  40601  fprodaddrecnncnvlem  40603  dvsinax  40607  fperdvper  40613  dvcosax  40621  ioodvbdlimc1lem1  40626  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  dvnmul  40638  dvnprodlem1  40641  dvnprodlem2  40642  dvnprodlem3  40643  itgsinexp  40650  itgcoscmulx  40664  itgsincmulx  40669  itgsubsticclem  40670  itgsubsticc  40671  itgiccshift  40675  stoweidlem7  40703  stoweidlem17  40713  stoweidlem32  40728  stoweidlem34  40730  wallispilem4  40764  wallispilem5  40765  wallispi  40766  wallispi2lem1  40767  wallispi2lem2  40768  wallispi2  40769  stirlinglem1  40770  stirlinglem2  40771  stirlinglem3  40772  stirlinglem4  40773  stirlinglem5  40774  stirlinglem7  40776  stirlinglem8  40777  stirlinglem10  40779  stirlinglem11  40780  stirlinglem12  40781  stirlinglem13  40782  stirlinglem14  40783  stirlinglem15  40784  dirkerval2  40790  dirkercncflem2  40800  fourierdlem7  40810  fourierdlem13  40816  fourierdlem14  40817  fourierdlem16  40819  fourierdlem18  40821  fourierdlem19  40822  fourierdlem21  40824  fourierdlem22  40825  fourierdlem26  40829  fourierdlem37  40840  fourierdlem39  40842  fourierdlem41  40844  fourierdlem48  40850  fourierdlem49  40851  fourierdlem50  40852  fourierdlem51  40853  fourierdlem53  40855  fourierdlem62  40864  fourierdlem63  40865  fourierdlem65  40867  fourierdlem73  40875  fourierdlem74  40876  fourierdlem75  40877  fourierdlem76  40878  fourierdlem79  40881  fourierdlem81  40883  fourierdlem82  40884  fourierdlem83  40885  fourierdlem84  40886  fourierdlem88  40890  fourierdlem89  40891  fourierdlem90  40892  fourierdlem91  40893  fourierdlem92  40894  fourierdlem93  40895  fourierdlem97  40899  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  fourierdlem111  40913  fourierdlem112  40914  fouriersw  40927  elaa2lem  40929  etransclem1  40931  etransclem12  40942  etransclem13  40943  etransclem17  40947  etransclem18  40948  etransclem21  40951  etransclem27  40957  etransclem31  40961  etransclem32  40962  etransclem33  40963  etransclem35  40965  etransclem46  40976  etransclem48  40978  rrxtopnfi  40985  salgenval  41020  sge0val  41062  sge0z  41071  sge0snmpt  41079  sge0xp  41125  nnfoctbdjlem  41151  psmeasurelem  41166  psmeasure  41167  meaiuninclem  41176  meaiininclem  41182  omeiunltfirp  41215  carageniuncllem1  41217  carageniuncllem2  41218  caratheodorylem1  41222  0ome  41225  vonval  41236  ovnval  41237  ovnval2  41241  hoicvr  41244  ovnval2b  41248  hoiprodcl2  41251  ovnlecvr  41254  ovncvrrp  41260  ovn0lem  41261  ovnsubaddlem1  41266  hsphoif  41272  hoidmvval  41273  hsphoival  41275  hoidmv1le  41290  hoidmvlelem3  41293  ovnhoilem1  41297  ovnhoilem2  41298  hoidifhspval  41304  hspval  41305  ovncvr2  41307  hoidifhspval2  41311  hoidifhspval3  41315  hspmbllem2  41323  ovnsubadd2lem  41341  vonioolem2  41377  vonicclem2  41380  issmflem  41418  smfid  41443  fvmptrab  41882  fvmptrabdm  41883  iccpval  41926  fmtno  42016  prmdvdsfmtnof1  42074  upwlksfval  42284  sprval  42297  sprsymrelfv  42312  uspgrsprfv  42321  clintopval  42408  assintopval  42409  c0mgm  42477  c0mhm  42478  c0snmgmhm  42482  c0snmhm  42483  zrrnghm  42485  rngcvalALTV  42529  rngcval  42530  rngcidALTV  42559  zrinitorngc  42568  zrtermorngc  42569  ringcvalALTV  42575  ringcval  42576  funcringcsetcALTV2lem1  42604  ringcidALTV  42622  funcringcsetclem1ALTV  42627  zrtermoringc  42638  rhmsubcALTVlem3  42674  scmsuppss  42721  ply1mulgsum  42746  lincop  42765  lincext3  42813  lindslinindsimp1  42814  lindsrng01  42825  lincresunit2  42835  lincresunit3lem1  42836  islindeps2  42840  fdivmptfv  42907  refdivmptfv  42908  bigoval  42911  blenval  42933  digfval  42959  amgmwlem  43119