Theorem fvmptd3 7020

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104   ↦ cmpt 5230  ‘cfv 6542

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fv 6550

This theorem is referenced by:  mptmpoopabbrd  8069  mptmpoopabbrdOLD  8071  undefval  8263  tz7.44-2  8409  fvdiagfn  8887  resixpfo  8932  fival  9409  cantnfp1lem1  9675  cantnfp1lem2  9676  cantnfp1lem3  9677  wemapwe  9694  rankvalb  9794  djulcl  9907  djuss  9917  1stinl  9924  2ndinl  9925  1stinr  9926  2ndinr  9927  fin23lem27  10325  isf34lem1  10369  canthp1lem2  10650  wuncval  10739  climrlim2  15495  summolem3  15664  prodmolem3  15881  iprodmul  15951  lcmfval  16562  iserodd  16772  mreacs  17606  isofval  17708  isofn  17726  cicfval  17748  initoval  17947  termoval  17948  zerooval  17949  pwsco1mhm  18749  pwsco2mhm  18750  vrmdfval  18773  galactghm  19313  symgfixfolem1  19347  pmtrval  19360  pmtrfv  19361  pmtrdifwrdellem3  19392  gsummhm2  19848  gsummpt1n0  19874  dprdfid  19928  lspval  20730  uvcval  21559  aspval  21646  evlslem3  21862  coe1tmfv1  22016  coe1tmfv2  22017  mat1rhmval  22201  scmatrhmval  22249  marepvval  22289  mply1topmatval  22526  mp2pm2mplem1  22528  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  tgval  22678  ntrval  22760  clsval  22761  opncldf2  22809  neival  22826  lpval  22863  1stcfb  23169  cnmpt11  23387  cnmpt21  23395  cnmptkp  23404  cnmptk1p  23409  ustval  23927  iunmbl  25302  cnmptlimc  25639  limccnp  25640  limcco  25642  coe1termlem  26007  coe1term  26008  ulmval  26128  pserulm  26170  efgh  26286  rlimcnp  26706  xrlimcnp  26709  dchrelbasd  26978  gausslemma2dlem4  27108  2lgslem1b  27131  madeval  27584  tgjustr  27992  mirval  28173  midf  28294  ismidb  28296  lmif  28303  islmib  28305  wksfval  29133  crctcshwlkn0lem2  29332  crctcshwlkn0lem3  29333  wwlks  29356  wlkiswwlks2lem2  29391  wlkswwlksf1o  29400  clwwlk  29503  clwlkclwwlkf1  29530  numclwlk2lem2fv  29898  spanval  30853  fsuppcurry1  32217  fsuppcurry2  32218  fzto1stfv1  32530  tocycval  32537  qusrn  32794  ghmquskerlem1  32802  elrspunidl  32820  elrspunsn  32821  prmidlval  32829  rprmval  32907  ply1gsumz  32944  r1plmhm  32955  ply1degltdimlem  32995  evls1fldgencl  33033  evls1maprhm  33048  evls1maplmhm  33049  ply1annidllem  33051  algextdeglem7  33068  rhmpreimacnlem  33162  indv  33308  esumcvg  33382  omsval  33590  eulerpartlemgvv  33673  cndprobval  33730  reprval  33920  hgt750lemb  33966  satfvsuc  34650  sat1el2xp  34668  fmlasuc0  34673  climlec3  35007  fwddifval  35438  knoppcnlem1  35672  knoppcnlem9  35680  unbdqndv2lem2  35689  knoppndvlem4  35694  knoppndvlem6  35696  bj-diagval  36358  bj-endval  36499  heiborlem4  36985  heiborlem6  36987  pclvalN  39064  frlmsnic  41412  rhmmpl  41427  mplmapghm  41430  evlsvvval  41437  evlsbagval  41440  evlsmaprhm  41444  evlsevl  41445  selvvvval  41459  evlselv  41461  mhphflem  41470  prjspnfv01  41668  prjspner01  41669  prjspner1  41670  rabdiophlem2  41842  fphpdo  41857  monotoddzz  41984  dnnumch3lem  42090  pwssplit4  42133  hbtlem1  42167  rgspnval  42212  eliunov2  42732  fvmptiunrelexplb0d  42737  fvmptiunrelexplb1d  42739  dssmapfvd  43070  wessf1ornlem  44182  projf1o  44194  fmuldfeq  44597  clim1fr1  44615  mullimcf  44637  sumnnodd  44644  expfac  44671  fnlimfv  44677  fnlimfvre2  44691  fnlimabslt  44693  limsuplt2  44767  liminfval  44773  limsupge  44775  cncfshift  44888  cncfiooicclem1  44907  fprodsubrecnncnvlem  44921  fprodaddrecnncnvlem  44923  ioodvbdlimc1lem1  44945  ioodvbdlimc1lem2  44946  dvnmul  44957  dvnprodlem1  44960  dvnprodlem2  44961  dvnprodlem3  44962  itgsinexp  44969  stoweidlem7  45021  stoweidlem17  45031  stoweidlem26  45040  stoweidlem30  45044  stoweidlem31  45045  stoweidlem32  45046  stoweidlem34  45048  wallispilem4  45082  wallispi  45084  stirlinglem3  45090  stirlinglem5  45092  stirlinglem7  45094  stirlinglem10  45097  dirkercncflem2  45118  etransclem1  45249  etransclem12  45260  etransclem27  45275  etransclem46  45294  etransclem48  45296  sge0snmptf  45451  nnfoctbdjlem  45469  psmeasurelem  45484  psmeasure  45485  meaiuninclem  45494  meaiininclem  45500  carageniuncllem1  45535  carageniuncllem2  45536  caratheodorylem1  45540  0ome  45543  vonval  45554  ovnval  45555  ovnval2b  45566  hoiprodcl2  45569  ovnlecvr  45572  ovncvrrp  45578  ovnsubaddlem1  45584  hsphoif  45590  hoidmvval  45591  hsphoival  45593  ovnhoilem1  45615  hoidifhspval  45622  hspval  45623  ovncvr2  45625  hspmbllem2  45641  ovnsubadd2lem  45659  vonioolem2  45695  vonicclem2  45698  issmflem  45741  smflimsuplem1  45834  smflimsuplem5  45838  smflimsuplem7  45840  fvmptrabdm  46299  sprsymrelfv  46460  prproropf1olem4  46472  fmtno  46495  prmdvdsfmtnof1  46553  upwlksfval  46811  uspgrsprfv  46821  assintopval  46881  lincop  47176  linc1  47193  lincext3  47224  el0ldep  47234  lincresunit2  47246  lincresunit3lem1  47247  blenval  47344  digfval  47370  itcoval  47434  ackval0012  47462  ackval1012  47463  ackval2012  47464  ackval3012  47465  lines  47504  spheres  47519