Theorem fvmptd3 6993

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5178  ‘cfv 6515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-iota 6471  df-fun 6517  df-fv 6523

This theorem is referenced by:  mptmpoopabbrd  8055  undefval  8250  tz7.44-2  8371  fsetfocdm  8835  fvdiagfn  8866  resixpfo  8911  fival  9351  cantnfp1lem1  9626  cantnfp1lem2  9627  cantnfp1lem3  9628  wemapwe  9645  rankvalb  9748  djulcl  9861  djuss  9871  1stinl  9878  2ndinl  9879  1stinr  9880  2ndinr  9881  fin23lem27  10278  isf34lem1  10322  canthp1lem2  10604  wuncval  10693  indv  12190  climrlim2  15564  summolem3  15731  prodmolem3  15953  iprodmul  16023  lcmfval  16645  iserodd  16861  mreacs  17680  isofval  17780  isofn  17798  cicfval  17820  initoval  18016  termoval  18017  zerooval  18018  pwsco1mhm  18856  pwsco2mhm  18857  vrmdfval  18880  ghmqusnsglem1  19310  ghmquskerlem1  19313  galactghm  19434  symgfixfolem1  19468  pmtrval  19481  pmtrfv  19482  pmtrdifwrdellem3  19513  gsummhm2  19969  gsummpt1n0  19995  dprdfid  20049  rgspnval  20648  lspval  21029  uvcval  21824  aspval  21911  evlslem3  22120  evlsvvval  22133  mplmapghm  22162  evlsmaprhm  22171  evlsevl  22172  selvvvval  22182  psdmplcl  22214  psdadd  22215  psdmul  22218  psdmvr  22221  coe1tmfv1  22324  coe1tmfv2  22325  evls1maprhm  22426  evls1maplmhm  22427  rhmmpl  22430  rhmply1vr1  22434  rhmply1vsca  22435  mat1rhmval  22526  scmatrhmval  22574  marepvval  22614  mply1topmatval  22851  mp2pm2mplem1  22853  chfacfscmulgsum  22907  chfacfpmmulgsum  22911  tgval  23002  ntrval  23083  clsval  23084  opncldf2  23132  neival  23149  lpval  23186  1stcfb  23492  cnmpt11  23710  cnmpt21  23718  cnmptkp  23727  cnmptk1p  23732  ustval  24250  iunmbl  25602  cnmptlimc  25939  limccnp  25940  limcco  25942  coe1termlem  26305  coe1term  26306  ulmval  26430  pserulm  26472  efgh  26593  rlimcnp  27017  xrlimcnp  27020  dchrelbasd  27290  gausslemma2dlem4  27420  2lgslem1b  27443  madeval  27912  abssval  28319  tgjustr  28630  mirval  28811  midf  28932  ismidb  28934  lmif  28941  islmib  28943  wksfval  29766  crctcshwlkn0lem2  29967  crctcshwlkn0lem3  29968  wwlks  29991  wlkiswwlks2lem2  30026  wlkswwlksf1o  30035  clwwlk  30141  clwlkclwwlkf1  30168  numclwlk2lem2fv  30536  spanval  31492  fsuppcurry1  32886  fsuppcurry2  32887  mndlactf1  33164  mndlactfo  33165  mndractf1  33166  mndractfo  33167  mndlactf1o  33168  mndractf1o  33169  gsummulsubdishift1s  33210  gsummulsubdishift2s  33211  gsumwrd2dccat  33218  fzto1stfv1  33241  tocycval  33248  fxpsubm  33312  fxpsubg  33313  fxpsubrg  33314  fxpsdrg  33315  elrgspnlem1  33383  elrgspnlem2  33384  elrgspnsubrunlem2  33389  rlocf1  33415  qusrn  33555  elrspunidl  33574  elrspunsn  33575  prmidlval  33583  rprmval  33672  zringfrac  33710  ply1gsumz  33755  r1plmhm  33766  0mplrim  33771  selvply1rhmlema  33775  selvply1rhmlemb  33776  selvply1rhmlem3  33779  selvply1rhmlem5  33781  extvfvcl  33793  mplvrpmrhm  33804  psrmonmul2  33808  psrmonprod  33809  esplyfvaln  33831  vietadeg1  33835  ply1degltdimlem  33879  lactlmhm  33891  evls1fldgencl  33927  fldextrspunlsplem  33930  fldextrspunlsp  33931  ply1annidllem  33958  algextdeglem7  33980  rhmpreimacnlem  34141  esumcvg  34343  omsval  34550  eulerpartlemgvv  34633  cndprobval  34690  reprval  34864  hgt750lemb  34910  fineqvnttrclselem2  35378  fineqvnttrclselem3  35379  fineqvnttrclse  35380  satfvsuc  35671  sat1el2xp  35689  fmlasuc0  35694  climlec3  36044  fwddifval  36472  knoppcnlem1  36891  knoppcnlem9  36899  unbdqndv2lem2  36908  knoppndvlem4  36913  knoppndvlem6  36915  bj-diagval  37626  bj-endval  37767  heiborlem4  38273  heiborlem6  38275  pclvalN  40474  frlmsnic  43118  rhmpsr  43125  evlsbagval  43128  evlselv  43131  mhphflem  43138  prjspnfv01  43166  prjspner01  43167  prjspner1  43168  rabdiophlem2  43339  fphpdo  43354  monotoddzz  43480  dnnumch3lem  43583  pwssplit4  43626  hbtlem1  43660  eliunov2  44215  fvmptiunrelexplb0d  44220  fvmptiunrelexplb1d  44222  dssmapfvd  44553  wessf1ornlem  45723  projf1o  45734  fmuldfeq  46119  clim1fr1  46137  mullimcf  46159  sumnnodd  46166  expfac  46191  fnlimfv  46197  fnlimfvre2  46211  fnlimabslt  46213  limsuplt2  46287  liminfval  46293  limsupge  46295  cncfshift  46408  cncfiooicclem1  46427  fprodsubrecnncnvlem  46441  fprodaddrecnncnvlem  46443  ioodvbdlimc1lem1  46465  ioodvbdlimc1lem2  46466  dvnmul  46477  dvnprodlem1  46480  dvnprodlem2  46481  dvnprodlem3  46482  itgsinexp  46489  stoweidlem7  46541  stoweidlem17  46551  stoweidlem26  46560  stoweidlem30  46564  stoweidlem31  46565  stoweidlem32  46566  stoweidlem34  46568  wallispilem4  46602  wallispi  46604  stirlinglem3  46610  stirlinglem5  46612  stirlinglem7  46614  stirlinglem10  46617  dirkercncflem2  46638  fourierdlem48  46688  fourierdlem49  46689  etransclem1  46769  etransclem12  46780  etransclem27  46795  etransclem46  46814  etransclem48  46816  sge0snmptf  46971  nnfoctbdjlem  46989  psmeasurelem  47004  psmeasure  47005  meaiuninclem  47014  meaiininclem  47020  carageniuncllem1  47055  carageniuncllem2  47056  caratheodorylem1  47060  0ome  47063  vonval  47074  ovnval  47075  ovnval2b  47086  hoiprodcl2  47089  ovnlecvr  47092  ovncvrrp  47098  ovnsubaddlem1  47104  hsphoif  47110  hoidmvval  47111  hsphoival  47113  ovnhoilem1  47135  hoidifhspval  47142  hspval  47143  ovncvr2  47145  hspmbllem2  47161  ovnsubadd2lem  47179  vonioolem2  47215  vonicclem2  47218  issmflem  47261  smflimsuplem1  47354  smflimsuplem5  47358  smflimsuplem7  47360  fvmptrabdm  47847  sprsymrelfv  48060  prproropf1olem4  48072  fmtno  48098  prmdvdsfmtnof1  48156  ppivalnn  48201  upwlksfval  48717  uspgrsprfv  48727  assintopval  48787  lincop  48990  linc1  49007  lincext3  49038  el0ldep  49048  lincresunit2  49060  lincresunit3lem1  49061  blenval  49153  digfval  49179  itcoval  49243  ackval0012  49271  ackval1012  49272  ackval2012  49273  ackval3012  49274  lines  49313  spheres  49328  invfn  49611  fucoid  49929