Theorem fvmptd3 7039

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5225  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569

This theorem is referenced by:  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  mptmpoopabbrdOLDOLD  8108  undefval  8301  tz7.44-2  8447  fsetfocdm  8901  fvdiagfn  8931  resixpfo  8976  fival  9452  cantnfp1lem1  9718  cantnfp1lem2  9719  cantnfp1lem3  9720  wemapwe  9737  rankvalb  9837  djulcl  9950  djuss  9960  1stinl  9967  2ndinl  9968  1stinr  9969  2ndinr  9970  fin23lem27  10368  isf34lem1  10412  canthp1lem2  10693  wuncval  10782  climrlim2  15583  summolem3  15750  prodmolem3  15969  iprodmul  16039  lcmfval  16658  iserodd  16873  mreacs  17701  isofval  17801  isofn  17819  cicfval  17841  initoval  18038  termoval  18039  zerooval  18040  pwsco1mhm  18845  pwsco2mhm  18846  vrmdfval  18869  ghmqusnsglem1  19298  ghmquskerlem1  19301  galactghm  19422  symgfixfolem1  19456  pmtrval  19469  pmtrfv  19470  pmtrdifwrdellem3  19501  gsummhm2  19957  gsummpt1n0  19983  dprdfid  20037  rgspnval  20612  lspval  20973  uvcval  21805  aspval  21893  evlslem3  22104  psdmplcl  22166  psdadd  22167  psdmul  22170  psdmvr  22173  coe1tmfv1  22277  coe1tmfv2  22278  evls1maprhm  22380  evls1maplmhm  22381  rhmmpl  22387  rhmply1vr1  22391  rhmply1vsca  22392  mat1rhmval  22485  scmatrhmval  22533  marepvval  22573  mply1topmatval  22810  mp2pm2mplem1  22812  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  tgval  22962  ntrval  23044  clsval  23045  opncldf2  23093  neival  23110  lpval  23147  1stcfb  23453  cnmpt11  23671  cnmpt21  23679  cnmptkp  23688  cnmptk1p  23693  ustval  24211  iunmbl  25588  cnmptlimc  25925  limccnp  25926  limcco  25928  coe1termlem  26297  coe1term  26298  ulmval  26423  pserulm  26465  efgh  26583  rlimcnp  27008  xrlimcnp  27011  dchrelbasd  27283  gausslemma2dlem4  27413  2lgslem1b  27436  madeval  27891  abssval  28263  tgjustr  28482  mirval  28663  midf  28784  ismidb  28786  lmif  28793  islmib  28795  wksfval  29627  crctcshwlkn0lem2  29831  crctcshwlkn0lem3  29832  wwlks  29855  wlkiswwlks2lem2  29890  wlkswwlksf1o  29899  clwwlk  30002  clwlkclwwlkf1  30029  numclwlk2lem2fv  30397  spanval  31352  fsuppcurry1  32736  fsuppcurry2  32737  indv  32837  mndlactf1  33031  mndlactfo  33032  mndractf1  33033  mndractfo  33034  mndlactf1o  33035  mndractf1o  33036  gsumwrd2dccat  33070  fzto1stfv1  33121  tocycval  33128  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnsubrunlem2  33252  rlocf1  33277  qusrn  33437  elrspunidl  33456  elrspunsn  33457  prmidlval  33465  rprmval  33544  zringfrac  33582  ply1gsumz  33619  r1plmhm  33630  ply1degltdimlem  33673  lactlmhm  33685  evls1fldgencl  33720  fldextrspunlsplem  33723  fldextrspunlsp  33724  ply1annidllem  33744  algextdeglem7  33764  rhmpreimacnlem  33883  esumcvg  34087  omsval  34295  eulerpartlemgvv  34378  cndprobval  34435  reprval  34625  hgt750lemb  34671  satfvsuc  35366  sat1el2xp  35384  fmlasuc0  35389  climlec3  35734  fwddifval  36163  knoppcnlem1  36494  knoppcnlem9  36502  unbdqndv2lem2  36511  knoppndvlem4  36516  knoppndvlem6  36518  bj-diagval  37175  bj-endval  37316  heiborlem4  37821  heiborlem6  37823  pclvalN  39892  frlmsnic  42550  rhmpsr  42562  mplmapghm  42566  evlsvvval  42573  evlsbagval  42576  evlsmaprhm  42580  evlsevl  42581  selvvvval  42595  evlselv  42597  mhphflem  42606  prjspnfv01  42634  prjspner01  42635  prjspner1  42636  rabdiophlem2  42813  fphpdo  42828  monotoddzz  42955  dnnumch3lem  43058  pwssplit4  43101  hbtlem1  43135  eliunov2  43692  fvmptiunrelexplb0d  43697  fvmptiunrelexplb1d  43699  dssmapfvd  44030  wessf1ornlem  45190  projf1o  45202  fmuldfeq  45598  clim1fr1  45616  mullimcf  45638  sumnnodd  45645  expfac  45672  fnlimfv  45678  fnlimfvre2  45692  fnlimabslt  45694  limsuplt2  45768  liminfval  45774  limsupge  45776  cncfshift  45889  cncfiooicclem1  45908  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  itgsinexp  45970  stoweidlem7  46022  stoweidlem17  46032  stoweidlem26  46041  stoweidlem30  46045  stoweidlem31  46046  stoweidlem32  46047  stoweidlem34  46049  wallispilem4  46083  wallispi  46085  stirlinglem3  46091  stirlinglem5  46093  stirlinglem7  46095  stirlinglem10  46098  dirkercncflem2  46119  etransclem1  46250  etransclem12  46261  etransclem27  46276  etransclem46  46295  etransclem48  46297  sge0snmptf  46452  nnfoctbdjlem  46470  psmeasurelem  46485  psmeasure  46486  meaiuninclem  46495  meaiininclem  46501  carageniuncllem1  46536  carageniuncllem2  46537  caratheodorylem1  46541  0ome  46544  vonval  46555  ovnval  46556  ovnval2b  46567  hoiprodcl2  46570  ovnlecvr  46573  ovncvrrp  46579  ovnsubaddlem1  46585  hsphoif  46591  hoidmvval  46592  hsphoival  46594  ovnhoilem1  46616  hoidifhspval  46623  hspval  46624  ovncvr2  46626  hspmbllem2  46642  ovnsubadd2lem  46660  vonioolem2  46696  vonicclem2  46699  issmflem  46742  smflimsuplem1  46835  smflimsuplem5  46839  smflimsuplem7  46841  fvmptrabdm  47305  sprsymrelfv  47481  prproropf1olem4  47493  fmtno  47516  prmdvdsfmtnof1  47574  upwlksfval  48051  uspgrsprfv  48061  assintopval  48121  lincop  48325  linc1  48342  lincext3  48373  el0ldep  48383  lincresunit2  48395  lincresunit3lem1  48396  blenval  48492  digfval  48518  itcoval  48582  ackval0012  48610  ackval1012  48611  ackval2012  48612  ackval3012  48613  lines  48652  spheres  48667  fucoid  49043