Theorem fvmptd3 6960

Description: Deduction version of fvmpt 6937. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

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

Assertion

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

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

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

Proof of Theorem fvmptd3

Step	Hyp	Ref	Expression
1		fvmptd3.3	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
2		fvmptd3.4	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
3		fvmptd3.2	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4		fvmptd3.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
5	3, 4	fvmptg 6935	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
6	1, 2, 5	syl2anc 584	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5176  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6444  df-fun 6490  df-fv 6496

This theorem is referenced by:  mptmpoopabbrd  8020  mptmpoopabbrdOLD  8021  undefval  8214  tz7.44-2  8334  fsetfocdm  8793  fvdiagfn  8823  resixpfo  8868  fival  9305  cantnfp1lem1  9577  cantnfp1lem2  9578  cantnfp1lem3  9579  wemapwe  9596  rankvalb  9699  djulcl  9812  djuss  9822  1stinl  9829  2ndinl  9830  1stinr  9831  2ndinr  9832  fin23lem27  10228  isf34lem1  10272  canthp1lem2  10553  wuncval  10642  climrlim2  15458  summolem3  15625  prodmolem3  15844  iprodmul  15914  lcmfval  16536  iserodd  16751  mreacs  17568  isofval  17668  isofn  17686  cicfval  17708  initoval  17904  termoval  17905  zerooval  17906  pwsco1mhm  18744  pwsco2mhm  18745  vrmdfval  18768  ghmqusnsglem1  19196  ghmquskerlem1  19199  galactghm  19320  symgfixfolem1  19354  pmtrval  19367  pmtrfv  19368  pmtrdifwrdellem3  19399  gsummhm2  19855  gsummpt1n0  19881  dprdfid  19935  rgspnval  20531  lspval  20912  uvcval  21726  aspval  21814  evlslem3  22018  psdmplcl  22080  psdadd  22081  psdmul  22084  psdmvr  22087  coe1tmfv1  22191  coe1tmfv2  22192  evls1maprhm  22294  evls1maplmhm  22295  rhmmpl  22301  rhmply1vr1  22305  rhmply1vsca  22306  mat1rhmval  22397  scmatrhmval  22445  marepvval  22485  mply1topmatval  22722  mp2pm2mplem1  22724  chfacfscmulgsum  22778  chfacfpmmulgsum  22782  tgval  22873  ntrval  22954  clsval  22955  opncldf2  23003  neival  23020  lpval  23057  1stcfb  23363  cnmpt11  23581  cnmpt21  23589  cnmptkp  23598  cnmptk1p  23603  ustval  24121  iunmbl  25484  cnmptlimc  25821  limccnp  25822  limcco  25824  coe1termlem  26193  coe1term  26194  ulmval  26319  pserulm  26361  efgh  26480  rlimcnp  26905  xrlimcnp  26908  dchrelbasd  27180  gausslemma2dlem4  27310  2lgslem1b  27333  madeval  27796  abssval  28180  tgjustr  28455  mirval  28636  midf  28757  ismidb  28759  lmif  28766  islmib  28768  wksfval  29592  crctcshwlkn0lem2  29793  crctcshwlkn0lem3  29794  wwlks  29817  wlkiswwlks2lem2  29852  wlkswwlksf1o  29861  clwwlk  29967  clwlkclwwlkf1  29994  numclwlk2lem2fv  30362  spanval  31317  fsuppcurry1  32713  fsuppcurry2  32714  indv  32840  mndlactf1  33016  mndlactfo  33017  mndractf1  33018  mndractfo  33019  mndlactf1o  33020  mndractf1o  33021  gsumwrd2dccat  33056  fzto1stfv1  33079  tocycval  33086  fxpsubm  33150  fxpsubg  33151  fxpsubrg  33152  fxpsdrg  33153  elrgspnlem1  33218  elrgspnlem2  33219  elrgspnsubrunlem2  33224  rlocf1  33249  qusrn  33383  elrspunidl  33402  elrspunsn  33403  prmidlval  33411  rprmval  33490  zringfrac  33528  ply1gsumz  33568  r1plmhm  33579  extvfvcl  33589  mplvrpmrhm  33597  ply1degltdimlem  33658  lactlmhm  33670  evls1fldgencl  33706  fldextrspunlsplem  33709  fldextrspunlsp  33710  ply1annidllem  33737  algextdeglem7  33759  rhmpreimacnlem  33920  esumcvg  34122  omsval  34329  eulerpartlemgvv  34412  cndprobval  34469  reprval  34646  hgt750lemb  34692  fineqvnttrclselem2  35165  fineqvnttrclselem3  35166  fineqvnttrclse  35167  satfvsuc  35428  sat1el2xp  35446  fmlasuc0  35451  climlec3  35801  fwddifval  36229  knoppcnlem1  36560  knoppcnlem9  36568  unbdqndv2lem2  36577  knoppndvlem4  36582  knoppndvlem6  36584  bj-diagval  37241  bj-endval  37382  heiborlem4  37877  heiborlem6  37879  pclvalN  40012  frlmsnic  42661  rhmpsr  42673  mplmapghm  42677  evlsvvval  42684  evlsbagval  42687  evlsmaprhm  42691  evlsevl  42692  selvvvval  42706  evlselv  42708  mhphflem  42717  prjspnfv01  42745  prjspner01  42746  prjspner1  42747  rabdiophlem2  42922  fphpdo  42937  monotoddzz  43063  dnnumch3lem  43166  pwssplit4  43209  hbtlem1  43243  eliunov2  43799  fvmptiunrelexplb0d  43804  fvmptiunrelexplb1d  43806  dssmapfvd  44137  wessf1ornlem  45309  projf1o  45321  fmuldfeq  45710  clim1fr1  45728  mullimcf  45750  sumnnodd  45757  expfac  45782  fnlimfv  45788  fnlimfvre2  45802  fnlimabslt  45804  limsuplt2  45878  liminfval  45884  limsupge  45886  cncfshift  45999  cncfiooicclem1  46018  fprodsubrecnncnvlem  46032  fprodaddrecnncnvlem  46034  ioodvbdlimc1lem1  46056  ioodvbdlimc1lem2  46057  dvnmul  46068  dvnprodlem1  46071  dvnprodlem2  46072  dvnprodlem3  46073  itgsinexp  46080  stoweidlem7  46132  stoweidlem17  46142  stoweidlem26  46151  stoweidlem30  46155  stoweidlem31  46156  stoweidlem32  46157  stoweidlem34  46159  wallispilem4  46193  wallispi  46195  stirlinglem3  46201  stirlinglem5  46203  stirlinglem7  46205  stirlinglem10  46208  dirkercncflem2  46229  etransclem1  46360  etransclem12  46371  etransclem27  46386  etransclem46  46405  etransclem48  46407  sge0snmptf  46562  nnfoctbdjlem  46580  psmeasurelem  46595  psmeasure  46596  meaiuninclem  46605  meaiininclem  46611  carageniuncllem1  46646  carageniuncllem2  46647  caratheodorylem1  46651  0ome  46654  vonval  46665  ovnval  46666  ovnval2b  46677  hoiprodcl2  46680  ovnlecvr  46683  ovncvrrp  46689  ovnsubaddlem1  46695  hsphoif  46701  hoidmvval  46702  hsphoival  46704  ovnhoilem1  46726  hoidifhspval  46733  hspval  46734  ovncvr2  46736  hspmbllem2  46752  ovnsubadd2lem  46770  vonioolem2  46806  vonicclem2  46809  issmflem  46852  smflimsuplem1  46945  smflimsuplem5  46949  smflimsuplem7  46951  fvmptrabdm  47420  sprsymrelfv  47621  prproropf1olem4  47633  fmtno  47656  prmdvdsfmtnof1  47714  upwlksfval  48262  uspgrsprfv  48272  assintopval  48332  lincop  48536  linc1  48553  lincext3  48584  el0ldep  48594  lincresunit2  48606  lincresunit3lem1  48607  blenval  48699  digfval  48725  itcoval  48789  ackval0012  48817  ackval1012  48818  ackval2012  48819  ackval3012  48820  lines  48859  spheres  48874  invfn  49158  fucoid  49476