Theorem fvmptd3 6898

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   ↦ cmpt 5157  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441

This theorem is referenced by:  mptmpoopabbrd  7921  mptmpoopabbrdOLD  7923  undefval  8092  tz7.44-2  8238  fvdiagfn  8679  resixpfo  8724  fival  9171  cantnfp1lem1  9436  cantnfp1lem2  9437  cantnfp1lem3  9438  wemapwe  9455  rankvalb  9555  djulcl  9668  djuss  9678  1stinl  9685  2ndinl  9686  1stinr  9687  2ndinr  9688  fin23lem27  10084  isf34lem1  10128  canthp1lem2  10409  wuncval  10498  climrlim2  15256  summolem3  15426  prodmolem3  15643  iprodmul  15713  lcmfval  16326  iserodd  16536  mreacs  17367  isofval  17469  isofn  17487  cicfval  17509  initoval  17708  termoval  17709  zerooval  17710  pwsco1mhm  18470  pwsco2mhm  18471  vrmdfval  18495  galactghm  19012  symgfixfolem1  19046  pmtrval  19059  pmtrfv  19060  pmtrdifwrdellem3  19091  gsummhm2  19540  gsummpt1n0  19566  dprdfid  19620  lspval  20237  uvcval  20992  aspval  21077  evlslem3  21290  coe1tmfv1  21445  coe1tmfv2  21446  mat1rhmval  21628  scmatrhmval  21676  marepvval  21716  mply1topmatval  21953  mp2pm2mplem1  21955  chfacfscmulgsum  22009  chfacfpmmulgsum  22013  tgval  22105  ntrval  22187  clsval  22188  opncldf2  22236  neival  22253  lpval  22290  1stcfb  22596  cnmpt11  22814  cnmpt21  22822  cnmptkp  22831  cnmptk1p  22836  ustval  23354  iunmbl  24717  cnmptlimc  25054  limccnp  25055  limcco  25057  coe1termlem  25419  coe1term  25420  ulmval  25539  pserulm  25581  efgh  25697  rlimcnp  26115  xrlimcnp  26118  dchrelbasd  26387  gausslemma2dlem4  26517  2lgslem1b  26540  tgjustr  26835  mirval  27016  midf  27137  ismidb  27139  lmif  27146  islmib  27148  wksfval  27976  crctcshwlkn0lem2  28176  crctcshwlkn0lem3  28177  wwlks  28200  wlkiswwlks2lem2  28235  wlkswwlksf1o  28244  clwwlk  28347  clwlkclwwlkf1  28374  numclwlk2lem2fv  28742  spanval  29695  fsuppcurry1  31060  fsuppcurry2  31061  fzto1stfv1  31368  tocycval  31375  elrspunidl  31606  prmidlval  31612  rprmval  31664  rhmpreimacnlem  31834  indv  31980  esumcvg  32054  omsval  32260  eulerpartlemgvv  32343  cndprobval  32400  reprval  32590  hgt750lemb  32636  satfvsuc  33323  sat1el2xp  33341  fmlasuc0  33346  climlec3  33699  madeval  34036  fwddifval  34464  knoppcnlem1  34673  knoppcnlem9  34681  unbdqndv2lem2  34690  knoppndvlem4  34695  knoppndvlem6  34697  bj-diagval  35345  bj-endval  35486  heiborlem4  35972  heiborlem6  35974  pclvalN  37904  frlmsnic  40263  evlsbagval  40275  mhphflem  40284  prjspnfv01  40461  prjspner01  40462  prjspner1  40463  rabdiophlem2  40624  fphpdo  40639  monotoddzz  40765  dnnumch3lem  40871  pwssplit4  40914  hbtlem1  40948  rgspnval  40993  eliunov2  41287  fvmptiunrelexplb0d  41292  fvmptiunrelexplb1d  41294  dssmapfvd  41625  wessf1ornlem  42722  projf1o  42736  fmuldfeq  43124  clim1fr1  43142  mullimcf  43164  sumnnodd  43171  expfac  43198  fnlimfv  43204  fnlimfvre2  43218  fnlimabslt  43220  limsuplt2  43294  liminfval  43300  limsupge  43302  cncfshift  43415  cncfiooicclem1  43434  fprodsubrecnncnvlem  43448  fprodaddrecnncnvlem  43450  ioodvbdlimc1lem1  43472  ioodvbdlimc1lem2  43473  dvnmul  43484  dvnprodlem1  43487  dvnprodlem2  43488  dvnprodlem3  43489  itgsinexp  43496  stoweidlem7  43548  stoweidlem17  43558  stoweidlem26  43567  stoweidlem30  43571  stoweidlem31  43572  stoweidlem32  43573  stoweidlem34  43575  wallispilem4  43609  wallispi  43611  stirlinglem3  43617  stirlinglem5  43619  stirlinglem7  43621  stirlinglem10  43624  dirkercncflem2  43645  etransclem1  43776  etransclem12  43787  etransclem27  43802  etransclem46  43821  etransclem48  43823  sge0snmptf  43975  nnfoctbdjlem  43993  psmeasurelem  44008  psmeasure  44009  meaiuninclem  44018  meaiininclem  44024  carageniuncllem1  44059  carageniuncllem2  44060  caratheodorylem1  44064  0ome  44067  vonval  44078  ovnval  44079  ovnval2b  44090  hoiprodcl2  44093  ovnlecvr  44096  ovncvrrp  44102  ovnsubaddlem1  44108  hsphoif  44114  hoidmvval  44115  hsphoival  44117  ovnhoilem1  44139  hoidifhspval  44146  hspval  44147  ovncvr2  44149  hspmbllem2  44165  ovnsubadd2lem  44183  vonioolem2  44219  vonicclem2  44222  issmflem  44263  smflimsuplem1  44353  smflimsuplem5  44357  smflimsuplem7  44359  fvmptrabdm  44785  sprsymrelfv  44946  prproropf1olem4  44958  fmtno  44981  prmdvdsfmtnof1  45039  upwlksfval  45297  uspgrsprfv  45307  assintopval  45399  lincop  45749  linc1  45766  lincext3  45797  el0ldep  45807  lincresunit2  45819  lincresunit3lem1  45820  blenval  45917  digfval  45943  itcoval  46007  ackval0012  46035  ackval1012  46036  ackval2012  46037  ackval3012  46038  lines  46077  spheres  46092