Theorem fvmptd3 7020

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ↦ cmpt 5197  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551

This theorem is used by:  mptmpoopabbrd  8087  undefval  8282  tz7.44-2  8403  fsetfocdm  8867  fvdiagfn  8898  resixpfo  8943  fival  9382  cantnfp1lem1  9657  cantnfp1lem2  9658  cantnfp1lem3  9659  wemapwe  9676  rankvalb  9779  djulcl  9915  djuss  9925  1stinl  9932  2ndinl  9933  1stinr  9934  2ndinr  9935  fin23lem27  10330  isf34lem1  10374  canthp1lem2  10656  wuncval  10745  indv  12238  climrlim2  15624  summolem3  15791  prodmolem3  16013  iprodmul  16083  lcmfval  16704  iserodd  16920  mreacs  17739  isofval  17839  isofn  17857  cicfval  17879  initoval  18075  termoval  18076  zerooval  18077  pwsco1mhm  18922  pwsco2mhm  18923  vrmdfval  18946  ghmqusnsglem1  19381  ghmquskerlem1  19384  galactghm  19505  symgfixfolem1  19539  pmtrval  19552  pmtrfv  19553  pmtrdifwrdellem3  19584  gsummhm2  20040  gsummpt1n0  20066  dprdfid  20120  rgspnval  20748  lspval  21133  prmidlval  21499  uvcval  21972  aspval  22059  evlslem3  22268  evlsvvval  22281  mplmapghm  22310  evlsmaprhm  22319  evlsevl  22320  selvvvval  22330  psdmplcl  22362  psdadd  22363  psdmul  22366  psdmvr  22369  coe1tmfv1  22472  coe1tmfv2  22473  evls1maprhm  22573  evls1maplmhm  22574  rhmmpl  22577  rhmply1vr1  22581  rhmply1vsca  22582  mat1rhmval  22673  scmatrhmval  22721  marepvval  22761  mply1topmatval  22998  mp2pm2mplem1  23000  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  tgval  23149  ntrval  23230  clsval  23231  opncldf2  23279  neival  23296  lpval  23333  1stcfb  23639  cnmpt11  23857  cnmpt21  23865  cnmptkp  23874  cnmptk1p  23879  ustval  24397  iunmbl  25749  cnmptlimc  26086  limccnp  26087  limcco  26089  coe1termlem  26452  coe1term  26453  ulmval  26580  pserulm  26622  efgh  26743  rlimcnp  27167  xrlimcnp  27170  dchrelbasd  27440  gausslemma2dlem4  27570  2lgslem1b  27593  madeval  28062  abssval  28469  tgjustr  28780  mirval  28969  tgplnfn  29094  plngval  29096  isplng  29097  midf  29122  ismidb  29124  lmif  29131  islmib  29133  brprlng  29225  wksfval  29996  crctcshwlkn0lem2  30197  crctcshwlkn0lem3  30198  wwlks  30221  wlkiswwlks2lem2  30256  wlkswwlksf1o  30265  clwwlk  30371  clwlkclwwlkf1  30398  numclwlk2lem2fv  30766  spanval  31722  fsuppcurry1  33106  fsuppcurry2  33107  mndlactf1  33377  mndlactfo  33378  mndractf1  33379  mndractfo  33380  mndlactf1o  33381  mndractf1o  33382  gsummulsubdishift1s  33421  gsummulsubdishift2s  33422  gsumwrd2dccat  33429  fzto1stfv1  33452  tocycval  33459  fxpsubm  33523  fxpsubg  33524  fxpsubrg  33525  fxpsdrg  33526  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnsubrunlem2  33599  rlocf1  33625  qusrn  33749  elrspunidl  33767  elrspunsn  33768  rprmval  33837  zringfrac  33875  ply1gsumz  33920  r1plmhm  33930  0mplrim  33935  selvply1rhmlema  33939  selvply1rhmlemb  33940  selvply1rhmlem3  33943  selvply1rhmlem5  33945  extvfvcl  33957  mplvrpmrhm  33968  psrmonmul2  33972  psrmonprod  33973  esplyfvaln  33995  vietadeg1  33999  ply1degltdimlem  34043  lactlmhm  34055  evls1fldgencl  34091  fldextrspunlsplem  34094  fldextrspunlsp  34095  ply1annidllem  34122  algextdeglem7  34144  rhmpreimacnlem  34305  esumcvg  34507  omsval  34715  eulerpartlemgvv  34798  cndprobval  34855  reprval  35029  hgt750lemb  35075  fineqvnttrclselem2  35559  fineqvnttrclselem3  35560  fineqvnttrclse  35561  satfvsuc  35874  sat1el2xp  35892  fmlasuc0  35897  climlec3  36247  fwddifval  36675  knoppcnlem1  37123  knoppcnlem9  37131  unbdqndv2lem2  37140  knoppndvlem4  37145  knoppndvlem6  37147  bj-diagval  37859  bj-endval  38000  heiborlem4  38506  heiborlem6  38508  pclvalN  40705  frlmsnic  43349  rhmpsr  43356  evlsbagval  43359  evlselv  43362  mhphflem  43369  prjspnfv01  43397  prjspner01  43398  prjspner1  43399  rabdiophlem2  43570  fphpdo  43585  monotoddzz  43711  dnnumch3lem  43814  pwssplit4  43857  hbtlem1  43891  eliunov2  44446  fvmptiunrelexplb0d  44451  fvmptiunrelexplb1d  44453  dssmapfvd  44784  wessf1ornlem  45944  projf1o  45955  fmuldfeq  46340  clim1fr1  46358  mullimcf  46380  sumnnodd  46387  expfac  46412  fnlimfv  46418  fnlimfvre2  46432  fnlimabslt  46434  limsuplt2  46508  liminfval  46514  limsupge  46516  cncfshift  46629  cncfiooicclem1  46648  fprodsubrecnncnvlem  46662  fprodaddrecnncnvlem  46664  ioodvbdlimc1lem1  46686  ioodvbdlimc1lem2  46687  dvnmul  46698  dvnprodlem1  46701  dvnprodlem2  46702  dvnprodlem3  46703  itgsinexp  46710  stoweidlem7  46762  stoweidlem17  46772  stoweidlem26  46781  stoweidlem30  46785  stoweidlem31  46786  stoweidlem32  46787  stoweidlem34  46789  wallispilem4  46823  wallispi  46825  stirlinglem3  46831  stirlinglem5  46833  stirlinglem7  46835  stirlinglem10  46838  dirkercncflem2  46859  fourierdlem48  46909  fourierdlem49  46910  etransclem1  46990  etransclem12  47001  etransclem27  47016  etransclem46  47035  etransclem48  47037  sge0snmptf  47192  nnfoctbdjlem  47210  psmeasurelem  47225  psmeasure  47226  meaiuninclem  47235  meaiininclem  47241  carageniuncllem1  47276  carageniuncllem2  47277  caratheodorylem1  47281  0ome  47284  vonval  47295  ovnval  47296  ovnval2b  47307  hoiprodcl2  47310  ovnlecvr  47313  ovncvrrp  47319  ovnsubaddlem1  47325  hsphoif  47331  hoidmvval  47332  hsphoival  47334  ovnhoilem1  47356  hoidifhspval  47363  hspval  47364  ovncvr2  47366  hspmbllem2  47382  ovnsubadd2lem  47400  vonioolem2  47436  vonicclem2  47439  issmflem  47482  smflimsuplem1  47575  smflimsuplem5  47579  smflimsuplem7  47581  fvmptrabdm  48071  sprsymrelfv  48284  prproropf1olem4  48296  fmtno  48322  prmdvdsfmtnof1  48380  ppivalnn  48425  upwlksfval  48941  uspgrsprfv  48951  assintopval  49011  lincop  49229  linc1  49246  lincext3  49277  el0ldep  49287  lincresunit2  49299  lincresunit3lem1  49300  blenval  49392  digfval  49418  itcoval  49482  ackval0012  49510  ackval1012  49511  ackval2012  49512  ackval3012  49513  lines  49552  spheres  49567  invfn  49849  fucoid  50167  crosspalti  50689  crossp3i  50690