Theorem fvmptd3 7015

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ↦ cmpt 5193  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is referenced by:  mptmpoopabbrd  8079  undefval  8274  tz7.44-2  8395  fsetfocdm  8859  fvdiagfn  8890  resixpfo  8935  fival  9373  cantnfp1lem1  9648  cantnfp1lem2  9649  cantnfp1lem3  9650  wemapwe  9667  rankvalb  9770  djulcl  9897  djuss  9907  1stinl  9914  2ndinl  9915  1stinr  9916  2ndinr  9917  fin23lem27  10313  isf34lem1  10357  canthp1lem2  10639  wuncval  10728  indv  12221  climrlim2  15600  summolem3  15767  prodmolem3  15989  iprodmul  16059  lcmfval  16680  iserodd  16896  mreacs  17715  isofval  17815  isofn  17833  cicfval  17855  initoval  18051  termoval  18052  zerooval  18053  pwsco1mhm  18892  pwsco2mhm  18893  vrmdfval  18916  ghmqusnsglem1  19351  ghmquskerlem1  19354  galactghm  19475  symgfixfolem1  19509  pmtrval  19522  pmtrfv  19523  pmtrdifwrdellem3  19554  gsummhm2  20010  gsummpt1n0  20036  dprdfid  20090  rgspnval  20698  lspval  21077  prmidlval  21443  uvcval  21916  aspval  22003  evlslem3  22212  evlsvvval  22225  mplmapghm  22254  evlsmaprhm  22263  evlsevl  22264  selvvvval  22274  psdmplcl  22306  psdadd  22307  psdmul  22310  psdmvr  22313  coe1tmfv1  22416  coe1tmfv2  22417  evls1maprhm  22517  evls1maplmhm  22518  rhmmpl  22521  rhmply1vr1  22525  rhmply1vsca  22526  mat1rhmval  22617  scmatrhmval  22665  marepvval  22705  mply1topmatval  22942  mp2pm2mplem1  22944  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  tgval  23093  ntrval  23174  clsval  23175  opncldf2  23223  neival  23240  lpval  23277  1stcfb  23583  cnmpt11  23801  cnmpt21  23809  cnmptkp  23818  cnmptk1p  23823  ustval  24341  iunmbl  25693  cnmptlimc  26030  limccnp  26031  limcco  26033  coe1termlem  26396  coe1term  26397  ulmval  26524  pserulm  26566  efgh  26687  rlimcnp  27111  xrlimcnp  27114  dchrelbasd  27384  gausslemma2dlem4  27514  2lgslem1b  27537  madeval  28006  abssval  28413  tgjustr  28724  mirval  28913  tgplnfn  29038  plngval  29040  isplng  29041  midf  29066  ismidb  29068  lmif  29075  islmib  29077  brprlng  29169  wksfval  29940  crctcshwlkn0lem2  30141  crctcshwlkn0lem3  30142  wwlks  30165  wlkiswwlks2lem2  30200  wlkswwlksf1o  30209  clwwlk  30315  clwlkclwwlkf1  30342  numclwlk2lem2fv  30710  spanval  31666  fsuppcurry1  33050  fsuppcurry2  33051  mndlactf1  33327  mndlactfo  33328  mndractf1  33329  mndractfo  33330  mndlactf1o  33331  mndractf1o  33332  gsummulsubdishift1s  33371  gsummulsubdishift2s  33372  gsumwrd2dccat  33379  fzto1stfv1  33402  tocycval  33409  fxpsubm  33473  fxpsubg  33474  fxpsubrg  33475  fxpsdrg  33476  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnsubrunlem2  33549  rlocf1  33575  qusrn  33699  elrspunidl  33717  elrspunsn  33718  rprmval  33787  zringfrac  33825  ply1gsumz  33870  r1plmhm  33880  0mplrim  33885  selvply1rhmlema  33889  selvply1rhmlemb  33890  selvply1rhmlem3  33893  selvply1rhmlem5  33895  extvfvcl  33907  mplvrpmrhm  33918  psrmonmul2  33922  psrmonprod  33923  esplyfvaln  33945  vietadeg1  33949  ply1degltdimlem  33993  lactlmhm  34005  evls1fldgencl  34041  fldextrspunlsplem  34044  fldextrspunlsp  34045  ply1annidllem  34072  algextdeglem7  34094  rhmpreimacnlem  34255  esumcvg  34457  omsval  34664  eulerpartlemgvv  34747  cndprobval  34804  reprval  34978  hgt750lemb  35024  fineqvnttrclselem2  35516  fineqvnttrclselem3  35517  fineqvnttrclse  35518  satfvsuc  35834  sat1el2xp  35852  fmlasuc0  35857  climlec3  36207  fwddifval  36635  knoppcnlem1  37063  knoppcnlem9  37071  unbdqndv2lem2  37080  knoppndvlem4  37085  knoppndvlem6  37087  bj-diagval  37799  bj-endval  37940  heiborlem4  38446  heiborlem6  38448  pclvalN  40645  frlmsnic  43291  rhmpsr  43298  evlsbagval  43301  evlselv  43304  mhphflem  43311  prjspnfv01  43339  prjspner01  43340  prjspner1  43341  rabdiophlem2  43512  fphpdo  43527  monotoddzz  43653  dnnumch3lem  43756  pwssplit4  43799  hbtlem1  43833  eliunov2  44388  fvmptiunrelexplb0d  44393  fvmptiunrelexplb1d  44395  dssmapfvd  44726  wessf1ornlem  45886  projf1o  45897  fmuldfeq  46282  clim1fr1  46300  mullimcf  46322  sumnnodd  46329  expfac  46354  fnlimfv  46360  fnlimfvre2  46374  fnlimabslt  46376  limsuplt2  46450  liminfval  46456  limsupge  46458  cncfshift  46571  cncfiooicclem1  46590  fprodsubrecnncnvlem  46604  fprodaddrecnncnvlem  46606  ioodvbdlimc1lem1  46628  ioodvbdlimc1lem2  46629  dvnmul  46640  dvnprodlem1  46643  dvnprodlem2  46644  dvnprodlem3  46645  itgsinexp  46652  stoweidlem7  46704  stoweidlem17  46714  stoweidlem26  46723  stoweidlem30  46727  stoweidlem31  46728  stoweidlem32  46729  stoweidlem34  46731  wallispilem4  46765  wallispi  46767  stirlinglem3  46773  stirlinglem5  46775  stirlinglem7  46777  stirlinglem10  46780  dirkercncflem2  46801  fourierdlem48  46851  fourierdlem49  46852  etransclem1  46932  etransclem12  46943  etransclem27  46958  etransclem46  46977  etransclem48  46979  sge0snmptf  47134  nnfoctbdjlem  47152  psmeasurelem  47167  psmeasure  47168  meaiuninclem  47177  meaiininclem  47183  carageniuncllem1  47218  carageniuncllem2  47219  caratheodorylem1  47223  0ome  47226  vonval  47237  ovnval  47238  ovnval2b  47249  hoiprodcl2  47252  ovnlecvr  47255  ovncvrrp  47261  ovnsubaddlem1  47267  hsphoif  47273  hoidmvval  47274  hsphoival  47276  ovnhoilem1  47298  hoidifhspval  47305  hspval  47306  ovncvr2  47308  hspmbllem2  47324  ovnsubadd2lem  47342  vonioolem2  47378  vonicclem2  47381  issmflem  47424  smflimsuplem1  47517  smflimsuplem5  47521  smflimsuplem7  47523  fvmptrabdm  48013  sprsymrelfv  48226  prproropf1olem4  48238  fmtno  48264  prmdvdsfmtnof1  48322  ppivalnn  48367  upwlksfval  48883  uspgrsprfv  48893  assintopval  48953  lincop  49171  linc1  49188  lincext3  49219  el0ldep  49229  lincresunit2  49241  lincresunit3lem1  49242  blenval  49334  digfval  49360  itcoval  49424  ackval0012  49452  ackval1012  49453  ackval2012  49454  ackval3012  49455  lines  49494  spheres  49509  invfn  49791  fucoid  50109