Theorem fvmptd3 6957

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5176  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  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 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  mptmpoopabbrd  8022  mptmpoopabbrdOLD  8023  undefval  8216  tz7.44-2  8336  fsetfocdm  8795  fvdiagfn  8825  resixpfo  8870  fival  9321  cantnfp1lem1  9593  cantnfp1lem2  9594  cantnfp1lem3  9595  wemapwe  9612  rankvalb  9712  djulcl  9825  djuss  9835  1stinl  9842  2ndinl  9843  1stinr  9844  2ndinr  9845  fin23lem27  10241  isf34lem1  10285  canthp1lem2  10566  wuncval  10655  climrlim2  15472  summolem3  15639  prodmolem3  15858  iprodmul  15928  lcmfval  16550  iserodd  16765  mreacs  17582  isofval  17682  isofn  17700  cicfval  17722  initoval  17918  termoval  17919  zerooval  17920  pwsco1mhm  18724  pwsco2mhm  18725  vrmdfval  18748  ghmqusnsglem1  19177  ghmquskerlem1  19180  galactghm  19301  symgfixfolem1  19335  pmtrval  19348  pmtrfv  19349  pmtrdifwrdellem3  19380  gsummhm2  19836  gsummpt1n0  19862  dprdfid  19916  rgspnval  20515  lspval  20896  uvcval  21710  aspval  21798  evlslem3  22003  psdmplcl  22065  psdadd  22066  psdmul  22069  psdmvr  22072  coe1tmfv1  22176  coe1tmfv2  22177  evls1maprhm  22279  evls1maplmhm  22280  rhmmpl  22286  rhmply1vr1  22290  rhmply1vsca  22291  mat1rhmval  22382  scmatrhmval  22430  marepvval  22470  mply1topmatval  22707  mp2pm2mplem1  22709  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  tgval  22858  ntrval  22939  clsval  22940  opncldf2  22988  neival  23005  lpval  23042  1stcfb  23348  cnmpt11  23566  cnmpt21  23574  cnmptkp  23583  cnmptk1p  23588  ustval  24106  iunmbl  25470  cnmptlimc  25807  limccnp  25808  limcco  25810  coe1termlem  26179  coe1term  26180  ulmval  26305  pserulm  26347  efgh  26466  rlimcnp  26891  xrlimcnp  26894  dchrelbasd  27166  gausslemma2dlem4  27296  2lgslem1b  27319  madeval  27780  abssval  28164  tgjustr  28437  mirval  28618  midf  28739  ismidb  28741  lmif  28748  islmib  28750  wksfval  29573  crctcshwlkn0lem2  29774  crctcshwlkn0lem3  29775  wwlks  29798  wlkiswwlks2lem2  29833  wlkswwlksf1o  29842  clwwlk  29945  clwlkclwwlkf1  29972  numclwlk2lem2fv  30340  spanval  31295  fsuppcurry1  32681  fsuppcurry2  32682  indv  32808  mndlactf1  32993  mndlactfo  32994  mndractf1  32995  mndractfo  32996  mndlactf1o  32997  mndractf1o  32998  gsumwrd2dccat  33033  fzto1stfv1  33056  tocycval  33063  fxpsubm  33127  fxpsubg  33128  fxpsubrg  33129  fxpsdrg  33130  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnsubrunlem2  33201  rlocf1  33226  qusrn  33359  elrspunidl  33378  elrspunsn  33379  prmidlval  33387  rprmval  33466  zringfrac  33504  ply1gsumz  33543  r1plmhm  33554  ply1degltdimlem  33597  lactlmhm  33609  evls1fldgencl  33644  fldextrspunlsplem  33647  fldextrspunlsp  33648  ply1annidllem  33670  algextdeglem7  33692  rhmpreimacnlem  33853  esumcvg  34055  omsval  34263  eulerpartlemgvv  34346  cndprobval  34403  reprval  34580  hgt750lemb  34626  satfvsuc  35336  sat1el2xp  35354  fmlasuc0  35359  climlec3  35709  fwddifval  36138  knoppcnlem1  36469  knoppcnlem9  36477  unbdqndv2lem2  36486  knoppndvlem4  36491  knoppndvlem6  36493  bj-diagval  37150  bj-endval  37291  heiborlem4  37796  heiborlem6  37798  pclvalN  39872  frlmsnic  42516  rhmpsr  42528  mplmapghm  42532  evlsvvval  42539  evlsbagval  42542  evlsmaprhm  42546  evlsevl  42547  selvvvval  42561  evlselv  42563  mhphflem  42572  prjspnfv01  42600  prjspner01  42601  prjspner1  42602  rabdiophlem2  42778  fphpdo  42793  monotoddzz  42919  dnnumch3lem  43022  pwssplit4  43065  hbtlem1  43099  eliunov2  43655  fvmptiunrelexplb0d  43660  fvmptiunrelexplb1d  43662  dssmapfvd  43993  wessf1ornlem  45166  projf1o  45178  fmuldfeq  45568  clim1fr1  45586  mullimcf  45608  sumnnodd  45615  expfac  45642  fnlimfv  45648  fnlimfvre2  45662  fnlimabslt  45664  limsuplt2  45738  liminfval  45744  limsupge  45746  cncfshift  45859  cncfiooicclem1  45878  fprodsubrecnncnvlem  45892  fprodaddrecnncnvlem  45894  ioodvbdlimc1lem1  45916  ioodvbdlimc1lem2  45917  dvnmul  45928  dvnprodlem1  45931  dvnprodlem2  45932  dvnprodlem3  45933  itgsinexp  45940  stoweidlem7  45992  stoweidlem17  46002  stoweidlem26  46011  stoweidlem30  46015  stoweidlem31  46016  stoweidlem32  46017  stoweidlem34  46019  wallispilem4  46053  wallispi  46055  stirlinglem3  46061  stirlinglem5  46063  stirlinglem7  46065  stirlinglem10  46068  dirkercncflem2  46089  etransclem1  46220  etransclem12  46231  etransclem27  46246  etransclem46  46265  etransclem48  46267  sge0snmptf  46422  nnfoctbdjlem  46440  psmeasurelem  46455  psmeasure  46456  meaiuninclem  46465  meaiininclem  46471  carageniuncllem1  46506  carageniuncllem2  46507  caratheodorylem1  46511  0ome  46514  vonval  46525  ovnval  46526  ovnval2b  46537  hoiprodcl2  46540  ovnlecvr  46543  ovncvrrp  46549  ovnsubaddlem1  46555  hsphoif  46561  hoidmvval  46562  hsphoival  46564  ovnhoilem1  46586  hoidifhspval  46593  hspval  46594  ovncvr2  46596  hspmbllem2  46612  ovnsubadd2lem  46630  vonioolem2  46666  vonicclem2  46669  issmflem  46712  smflimsuplem1  46805  smflimsuplem5  46809  smflimsuplem7  46811  fvmptrabdm  47281  sprsymrelfv  47482  prproropf1olem4  47494  fmtno  47517  prmdvdsfmtnof1  47575  upwlksfval  48123  uspgrsprfv  48133  assintopval  48193  lincop  48397  linc1  48414  lincext3  48445  el0ldep  48455  lincresunit2  48467  lincresunit3lem1  48468  blenval  48560  digfval  48586  itcoval  48650  ackval0012  48678  ackval1012  48679  ackval2012  48680  ackval3012  48681  lines  48720  spheres  48735  invfn  49019  fucoid  49337