Theorem fvmptd3 6880

Description: Deduction version of fvmpt 6857. (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 6855	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
6	1, 2, 5	syl2anc 583	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ↦ cmpt 5153  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426

This theorem is referenced by:  mptmpoopabbrd  7894  undefval  8063  tz7.44-2  8209  fvdiagfn  8637  resixpfo  8682  fival  9101  cantnfp1lem1  9366  cantnfp1lem2  9367  cantnfp1lem3  9368  wemapwe  9385  rankvalb  9486  djulcl  9599  djuss  9609  1stinl  9616  2ndinl  9617  1stinr  9618  2ndinr  9619  fin23lem27  10015  isf34lem1  10059  canthp1lem2  10340  wuncval  10429  climrlim2  15184  summolem3  15354  prodmolem3  15571  iprodmul  15641  lcmfval  16254  iserodd  16464  mreacs  17284  isofval  17386  isofn  17404  cicfval  17426  initoval  17624  termoval  17625  zerooval  17626  pwsco1mhm  18385  pwsco2mhm  18386  vrmdfval  18410  galactghm  18927  symgfixfolem1  18961  pmtrval  18974  pmtrfv  18975  pmtrdifwrdellem3  19006  gsummhm2  19455  gsummpt1n0  19481  dprdfid  19535  lspval  20152  uvcval  20902  aspval  20987  evlslem3  21200  coe1tmfv1  21355  coe1tmfv2  21356  mat1rhmval  21536  scmatrhmval  21584  marepvval  21624  mply1topmatval  21861  mp2pm2mplem1  21863  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  tgval  22013  ntrval  22095  clsval  22096  opncldf2  22144  neival  22161  lpval  22198  1stcfb  22504  cnmpt11  22722  cnmpt21  22730  cnmptkp  22739  cnmptk1p  22744  ustval  23262  iunmbl  24622  cnmptlimc  24959  limccnp  24960  limcco  24962  coe1termlem  25324  coe1term  25325  ulmval  25444  pserulm  25486  efgh  25602  rlimcnp  26020  xrlimcnp  26023  dchrelbasd  26292  gausslemma2dlem4  26422  2lgslem1b  26445  tgjustr  26739  mirval  26920  midf  27041  ismidb  27043  lmif  27050  islmib  27052  wksfval  27879  crctcshwlkn0lem2  28077  crctcshwlkn0lem3  28078  wwlks  28101  wlkiswwlks2lem2  28136  wlkswwlksf1o  28145  clwwlk  28248  clwlkclwwlkf1  28275  numclwlk2lem2fv  28643  spanval  29596  fsuppcurry1  30962  fsuppcurry2  30963  fzto1stfv1  31270  tocycval  31277  elrspunidl  31508  prmidlval  31514  rprmval  31566  rhmpreimacnlem  31736  indv  31880  esumcvg  31954  omsval  32160  eulerpartlemgvv  32243  cndprobval  32300  reprval  32490  hgt750lemb  32536  satfvsuc  33223  sat1el2xp  33241  fmlasuc0  33246  climlec3  33605  madeval  33963  fwddifval  34391  knoppcnlem1  34600  knoppcnlem9  34608  unbdqndv2lem2  34617  knoppndvlem4  34622  knoppndvlem6  34624  bj-diagval  35272  bj-endval  35413  heiborlem4  35899  heiborlem6  35901  pclvalN  37831  frlmsnic  40188  evlsbagval  40198  mhphflem  40207  prjspnfv01  40382  prjspner01  40383  prjspner1  40384  rabdiophlem2  40540  fphpdo  40555  monotoddzz  40681  dnnumch3lem  40787  pwssplit4  40830  hbtlem1  40864  rgspnval  40909  eliunov2  41176  fvmptiunrelexplb0d  41181  fvmptiunrelexplb1d  41183  dssmapfvd  41514  wessf1ornlem  42611  projf1o  42625  fmuldfeq  43014  clim1fr1  43032  mullimcf  43054  sumnnodd  43061  expfac  43088  fnlimfv  43094  fnlimfvre2  43108  fnlimabslt  43110  limsuplt2  43184  liminfval  43190  limsupge  43192  cncfshift  43305  cncfiooicclem1  43324  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  dvnmul  43374  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  itgsinexp  43386  stoweidlem7  43438  stoweidlem17  43448  stoweidlem26  43457  stoweidlem30  43461  stoweidlem31  43462  stoweidlem32  43463  stoweidlem34  43465  wallispilem4  43499  wallispi  43501  stirlinglem3  43507  stirlinglem5  43509  stirlinglem7  43511  stirlinglem10  43514  dirkercncflem2  43535  etransclem1  43666  etransclem12  43677  etransclem27  43692  etransclem46  43711  etransclem48  43713  sge0snmptf  43865  nnfoctbdjlem  43883  psmeasurelem  43898  psmeasure  43899  meaiuninclem  43908  meaiininclem  43914  carageniuncllem1  43949  carageniuncllem2  43950  caratheodorylem1  43954  0ome  43957  vonval  43968  ovnval  43969  ovnval2b  43980  hoiprodcl2  43983  ovnlecvr  43986  ovncvrrp  43992  ovnsubaddlem1  43998  hsphoif  44004  hoidmvval  44005  hsphoival  44007  ovnhoilem1  44029  hoidifhspval  44036  hspval  44037  ovncvr2  44039  hspmbllem2  44055  ovnsubadd2lem  44073  vonioolem2  44109  vonicclem2  44112  issmflem  44150  smflimsuplem1  44240  smflimsuplem5  44244  smflimsuplem7  44246  fvmptrabdm  44672  sprsymrelfv  44834  prproropf1olem4  44846  fmtno  44869  prmdvdsfmtnof1  44927  upwlksfval  45185  uspgrsprfv  45195  assintopval  45287  lincop  45637  linc1  45654  lincext3  45685  el0ldep  45695  lincresunit2  45707  lincresunit3lem1  45708  blenval  45805  digfval  45831  itcoval  45895  ackval0012  45923  ackval1012  45924  ackval2012  45925  ackval3012  45926  lines  45965  spheres  45980