Theorem fvmptd 6768

Description: Deduction version of fvmpt 6761. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof shortened by AV, 29-Mar-2024.)

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	. 2 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))
2		fvmptd.2	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
3		fvmptd.3	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
4		fvmptd.4	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
5		nfv 1909	. 2 ⊢ Ⅎ𝑥𝜑
6		nfcv 2975	. 2 ⊢ Ⅎ𝑥𝐴
7		nfcv 2975	. 2 ⊢ Ⅎ𝑥𝐶
8	1, 2, 3, 4, 5, 6, 7	fvmptdf 6767	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1531   ∈ wcel 2108   ↦ cmpt 5137  ‘cfv 6348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356

This theorem is referenced by:  fvmptd2  6769  fvmptdv2  6779  fsplitfpar  7806  mpocurryvald  7928  ttukeylem3  9925  ccatval1  13922  ccatval1OLD  13923  ccatval2  13924  repswsymb  14128  relexp1g  14377  rtrclreclem2  14410  rtrclreclem4  14412  dfrtrcl2  14413  prmodvdslcmf  16375  prmgap  16387  prmgaplcm  16388  prmgapprmo  16390  prdsvscafval  16745  mrcval  16873  cidval  16940  subcid  17109  idfu2nd  17139  resf2nd  17157  fuccoval  17225  fucid  17233  homaval  17283  idaval  17310  setcid  17338  catcid  17355  estrcid  17376  funcestrcsetclem1  17382  funcsetcestrclem1  17396  prf1  17442  prf2  17444  curf1  17467  curf11  17468  curf2val  17472  hof2  17499  yonedalem4a  17517  vrmdval  18014  smndex1gbas  18059  smndex1gid  18060  smndex1n0mnd  18069  mulgnngsum  18225  pj1val  18813  dpjval  19170  sraval  19940  opsrval  20247  selvfval  20322  selvval  20323  mhpval  20325  cply1mul  20454  cply1coe0  20459  cply1coe0bi  20460  gsummoncoe1  20464  evls1sca  20478  frlmphl  20917  mvmulfv  21145  mavmulfv  21147  mdetuni0  21222  mat2pmatval  21324  m2cpm  21341  cpm2mval  21350  m2cpminvid2lem  21354  decpmatid  21370  decpmatmullem  21371  pmatcollpw2lem  21377  monmatcollpw  21379  pm2mpfval  21396  mp2pm2mplem4  21409  pm2mpmhmlem2  21419  chpmatval  21431  fcfval  22633  cnextfval  22662  utopsnneiplem  22848  rrxmvallem  23999  rrxmval  24000  taylpval  24947  lgamgulmlem2  25599  lgamcvglem  25609  logexprlim  25793  dchr1  25825  ishlg  26380  mirval  26433  mirfv  26434  ishpg  26537  lmif  26563  islmib  26565  lmodvslmhm  30681  psgnfzto1stlem  30735  tocycfv  30744  sgnsval  30796  madjusmdetlem2  31086  metidval  31123  pstmval  31128  qqhvval  31217  indval  31265  indfval  31268  esummulc1  31333  esumcvg  31338  ofcval  31351  sigagenval  31392  measinb  31473  omsfval  31545  omssubadd  31551  sitgfval  31592  eulerpartlemsv1  31607  eulerpartlems  31611  fibp1  31652  totprobd  31677  probmeasb  31681  dstrvprob  31722  dstfrvinc  31727  dstfrvclim1  31728  ballotlemfval  31740  ballotlemsv  31760  gsumnunsn  31804  signsply0  31814  signstfval  31827  fdvneggt  31864  fdvnegge  31866  itgexpif  31870  breprexplema  31894  vtsval  31901  logdivsqrle  31914  hgt750lemg  31918  afsval  31935  lpadval  31940  cvmliftlem9  32533  goel  32587  satf0suc  32616  sat1el2xp  32619  fmlafv  32620  fmla  32621  fmlasuc0  32624  ex-sategoelel  32661  ex-sategoelelomsuc  32666  mvrsval  32745  mrsubfval  32748  mrsubval  32749  msubfval  32764  msubval  32765  msrval  32778  fwddifval  33616  fwddifnval  33617  knoppcnlem1  33825  knoppcnlem4  33828  knoppcnlem6  33830  knoppcnlem7  33831  bj-imdirval2  34465  bj-fvmptunsn2  34532  bj-endval  34588  poimirlem1  34885  poimirlem2  34886  poimirlem5  34889  poimirlem6  34890  poimirlem7  34891  poimirlem10  34894  poimirlem11  34895  poimirlem12  34896  poimirlem19  34903  poimirlem22  34906  mblfinlem2  34922  areacirc  34979  tendopl2  37905  tendoi2  37923  erngplus2  37932  erngplus2-rN  37940  hlhilset  39062  itgpowd  39811  rfovfvd  40338  rfovfvfvd  40339  rfovcnvf1od  40340  rfovcnvfvd  40343  fsovfvd  40346  fsovfvfvd  40347  fsovcnvlem  40349  dssmapfv2d  40354  dssmapfv3d  40355  dssmapnvod  40356  clsk3nimkb  40380  dvgrat  40634  radcnvrat  40636  hashnzfzclim  40644  binomcxplemnn0  40671  binomcxplemrat  40672  binomcxplemfrat  40673  binomcxplemradcnv  40674  binomcxplemcvg  40676  binomcxplemdvsum  40677  binomcxplemnotnn0  40678  mapss2  41457  fmuldfeqlem1  41852  clim1fr1  41871  climrec  41873  climexp  41875  climneg  41880  divcnvg  41897  sumnnodd  41900  supcnvlimsup  42010  icccncfext  42159  cncfioobdlem  42168  fprodsubrecnncnvlem  42180  fprodaddrecnncnvlem  42182  dvsinax  42186  fperdvper  42192  dvcosax  42200  ioodvbdlimc1lem2  42206  ioodvbdlimc2lem  42208  dvnmul  42217  dvnprodlem1  42220  dvnprodlem2  42221  dvnprodlem3  42222  itgsinexp  42229  itgcoscmulx  42243  itgsincmulx  42248  itgsubsticclem  42249  itgsubsticc  42250  itgiccshift  42254  wallispilem5  42344  wallispi  42345  wallispi2lem1  42346  wallispi2lem2  42347  wallispi2  42348  stirlinglem1  42349  stirlinglem2  42350  stirlinglem3  42351  stirlinglem4  42352  stirlinglem5  42353  stirlinglem7  42355  stirlinglem8  42356  stirlinglem10  42358  stirlinglem11  42359  stirlinglem12  42360  stirlinglem13  42361  stirlinglem14  42362  stirlinglem15  42363  dirkerval2  42369  dirkercncflem2  42379  fourierdlem7  42389  fourierdlem13  42395  fourierdlem14  42396  fourierdlem16  42398  fourierdlem18  42400  fourierdlem19  42401  fourierdlem21  42403  fourierdlem22  42404  fourierdlem26  42408  fourierdlem37  42419  fourierdlem39  42421  fourierdlem41  42423  fourierdlem48  42429  fourierdlem49  42430  fourierdlem50  42431  fourierdlem51  42432  fourierdlem53  42434  fourierdlem62  42443  fourierdlem63  42444  fourierdlem65  42446  fourierdlem73  42454  fourierdlem74  42455  fourierdlem75  42456  fourierdlem76  42457  fourierdlem79  42460  fourierdlem81  42462  fourierdlem82  42463  fourierdlem83  42464  fourierdlem84  42465  fourierdlem88  42469  fourierdlem89  42470  fourierdlem90  42471  fourierdlem91  42472  fourierdlem92  42473  fourierdlem93  42474  fourierdlem97  42478  fourierdlem101  42482  fourierdlem103  42484  fourierdlem104  42485  fourierdlem111  42492  fourierdlem112  42493  fouriersw  42506  elaa2lem  42508  etransclem13  42522  etransclem17  42526  etransclem18  42527  etransclem21  42530  etransclem31  42540  etransclem32  42541  etransclem33  42542  etransclem35  42544  etransclem46  42555  etransclem48  42557  rrxtopnfi  42562  salgenval  42596  sge0val  42638  sge0z  42647  sge0snmpt  42655  sge0xp  42701  nnfoctbdjlem  42727  omeiunltfirp  42791  caratheodorylem1  42798  0ome  42801  ovnval2  42817  hoicvr  42820  ovncvrrp  42836  ovn0lem  42837  ovnsubaddlem1  42842  hsphoif  42848  hsphoival  42851  hoidmv1le  42866  hoidmvlelem3  42869  ovnhoilem2  42874  ovncvr2  42883  hoidifhspval2  42887  hoidifhspval3  42891  hspmbllem2  42899  smfid  43019  fvmptrab  43481  fundcmpsurinjlem3  43550  sprval  43631  prproropreud  43661  isomuspgrlem2a  43983  c0mgm  44170  c0mhm  44171  c0snmgmhm  44175  c0snmhm  44176  zrrnghm  44178  rngcvalALTV  44222  rngcidALTV  44252  zrinitorngc  44261  zrtermorngc  44262  ringcvalALTV  44268  funcringcsetcALTV2lem1  44297  ringcidALTV  44315  funcringcsetclem1ALTV  44320  zrtermoringc  44331  rhmsubcALTVlem3  44367  scmsuppss  44410  ply1mulgsum  44434  lindslinindsimp1  44502  lindsrng01  44513  islindeps2  44528  fdivmptfv  44595  refdivmptfv  44596  amgmwlem  44893