Theorem fvmptd3 7052

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ↦ cmpt 5249  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581

This theorem is referenced by:  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  mptmpoopabbrdOLDOLD  8124  undefval  8317  tz7.44-2  8463  fsetfocdm  8919  fvdiagfn  8949  resixpfo  8994  fival  9481  cantnfp1lem1  9747  cantnfp1lem2  9748  cantnfp1lem3  9749  wemapwe  9766  rankvalb  9866  djulcl  9979  djuss  9989  1stinl  9996  2ndinl  9997  1stinr  9998  2ndinr  9999  fin23lem27  10397  isf34lem1  10441  canthp1lem2  10722  wuncval  10811  climrlim2  15593  summolem3  15762  prodmolem3  15981  iprodmul  16051  lcmfval  16668  iserodd  16882  mreacs  17716  isofval  17818  isofn  17836  cicfval  17858  initoval  18060  termoval  18061  zerooval  18062  pwsco1mhm  18867  pwsco2mhm  18868  vrmdfval  18891  ghmqusnsglem1  19320  ghmquskerlem1  19323  galactghm  19446  symgfixfolem1  19480  pmtrval  19493  pmtrfv  19494  pmtrdifwrdellem3  19525  gsummhm2  19981  gsummpt1n0  20007  dprdfid  20061  lspval  20996  uvcval  21828  aspval  21916  evlslem3  22127  psdmplcl  22189  psdadd  22190  psdmul  22193  coe1tmfv1  22298  coe1tmfv2  22299  evls1maprhm  22401  evls1maplmhm  22402  rhmmpl  22408  rhmply1vr1  22412  rhmply1vsca  22413  mat1rhmval  22506  scmatrhmval  22554  marepvval  22594  mply1topmatval  22831  mp2pm2mplem1  22833  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  tgval  22983  ntrval  23065  clsval  23066  opncldf2  23114  neival  23131  lpval  23168  1stcfb  23474  cnmpt11  23692  cnmpt21  23700  cnmptkp  23709  cnmptk1p  23714  ustval  24232  iunmbl  25607  cnmptlimc  25945  limccnp  25946  limcco  25948  coe1termlem  26317  coe1term  26318  ulmval  26441  pserulm  26483  efgh  26601  rlimcnp  27026  xrlimcnp  27029  dchrelbasd  27301  gausslemma2dlem4  27431  2lgslem1b  27454  madeval  27909  abssval  28281  tgjustr  28500  mirval  28681  midf  28802  ismidb  28804  lmif  28811  islmib  28813  wksfval  29645  crctcshwlkn0lem2  29844  crctcshwlkn0lem3  29845  wwlks  29868  wlkiswwlks2lem2  29903  wlkswwlksf1o  29912  clwwlk  30015  clwlkclwwlkf1  30042  numclwlk2lem2fv  30410  spanval  31365  fsuppcurry1  32739  fsuppcurry2  32740  mndlactf1  33012  mndlactfo  33013  mndractf1  33014  mndractfo  33015  mndlactf1o  33016  mndractf1o  33017  fzto1stfv1  33094  tocycval  33101  rlocf1  33245  qusrn  33402  elrspunidl  33421  elrspunsn  33422  prmidlval  33430  rprmval  33509  zringfrac  33547  ply1gsumz  33584  r1plmhm  33595  ply1degltdimlem  33635  lactlmhm  33647  evls1fldgencl  33680  ply1annidllem  33694  algextdeglem7  33714  rhmpreimacnlem  33830  indv  33976  esumcvg  34050  omsval  34258  eulerpartlemgvv  34341  cndprobval  34398  reprval  34587  hgt750lemb  34633  satfvsuc  35329  sat1el2xp  35347  fmlasuc0  35352  climlec3  35696  fwddifval  36126  knoppcnlem1  36459  knoppcnlem9  36467  unbdqndv2lem2  36476  knoppndvlem4  36481  knoppndvlem6  36483  bj-diagval  37140  bj-endval  37281  heiborlem4  37774  heiborlem6  37776  pclvalN  39847  frlmsnic  42495  rhmpsr  42507  mplmapghm  42511  evlsvvval  42518  evlsbagval  42521  evlsmaprhm  42525  evlsevl  42526  selvvvval  42540  evlselv  42542  mhphflem  42551  prjspnfv01  42579  prjspner01  42580  prjspner1  42581  rabdiophlem2  42758  fphpdo  42773  monotoddzz  42900  dnnumch3lem  43003  pwssplit4  43046  hbtlem1  43080  rgspnval  43125  eliunov2  43641  fvmptiunrelexplb0d  43646  fvmptiunrelexplb1d  43648  dssmapfvd  43979  wessf1ornlem  45092  projf1o  45104  fmuldfeq  45504  clim1fr1  45522  mullimcf  45544  sumnnodd  45551  expfac  45578  fnlimfv  45584  fnlimfvre2  45598  fnlimabslt  45600  limsuplt2  45674  liminfval  45680  limsupge  45682  cncfshift  45795  cncfiooicclem1  45814  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  itgsinexp  45876  stoweidlem7  45928  stoweidlem17  45938  stoweidlem26  45947  stoweidlem30  45951  stoweidlem31  45952  stoweidlem32  45953  stoweidlem34  45955  wallispilem4  45989  wallispi  45991  stirlinglem3  45997  stirlinglem5  45999  stirlinglem7  46001  stirlinglem10  46004  dirkercncflem2  46025  etransclem1  46156  etransclem12  46167  etransclem27  46182  etransclem46  46201  etransclem48  46203  sge0snmptf  46358  nnfoctbdjlem  46376  psmeasurelem  46391  psmeasure  46392  meaiuninclem  46401  meaiininclem  46407  carageniuncllem1  46442  carageniuncllem2  46443  caratheodorylem1  46447  0ome  46450  vonval  46461  ovnval  46462  ovnval2b  46473  hoiprodcl2  46476  ovnlecvr  46479  ovncvrrp  46485  ovnsubaddlem1  46491  hsphoif  46497  hoidmvval  46498  hsphoival  46500  ovnhoilem1  46522  hoidifhspval  46529  hspval  46530  ovncvr2  46532  hspmbllem2  46548  ovnsubadd2lem  46566  vonioolem2  46602  vonicclem2  46605  issmflem  46648  smflimsuplem1  46741  smflimsuplem5  46745  smflimsuplem7  46747  fvmptrabdm  47208  sprsymrelfv  47368  prproropf1olem4  47380  fmtno  47403  prmdvdsfmtnof1  47461  upwlksfval  47858  uspgrsprfv  47868  assintopval  47928  lincop  48137  linc1  48154  lincext3  48185  el0ldep  48195  lincresunit2  48207  lincresunit3lem1  48208  blenval  48305  digfval  48331  itcoval  48395  ackval0012  48423  ackval1012  48424  ackval2012  48425  ackval3012  48426  lines  48465  spheres  48480