Theorem fvmptd3 6550

Description: Deduction version of fvmpt 6529. (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		nfcv 2969	. . 3 ⊢ Ⅎ𝑥𝐴
4		nfcv 2969	. . 3 ⊢ Ⅎ𝑥𝐶
5		fvmptd3.2	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
6		fvmptd3.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
7	3, 4, 5, 6	fvmptf 6548	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
8	1, 2, 7	syl2anc 581	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166   ↦ cmpt 4952  ‘cfv 6123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fv 6131

This theorem is referenced by:  mptmpt2opabbrd  7511  bropfvvvv  7521  resixpfo  8213  cantnfp1lem1  8852  cantnfp1lem2  8853  cantnfp1lem3  8854  wemapwe  8871  rankvalb  8937  fin23lem27  9465  canthp1lem2  9790  wuncval  9879  climrlim2  14655  summolem3  14822  prodmolem3  15036  iprodmul  15106  lcmfval  15707  iserodd  15911  mreacs  16671  isofval  16769  isofn  16787  pwsco1mhm  17723  pwsco2mhm  17724  vrmdfval  17747  galactghm  18173  symgfixfolem1  18208  pmtrfv  18222  pmtrdifwrdellem3  18253  gsummhm2  18692  gsummpt1n0  18717  dprdfid  18770  lspval  19334  aspval  19689  evlslem3  19874  coe1tmfv1  20004  coe1tmfv2  20005  marepvval  20741  mply1topmatval  20979  mp2pm2mplem1  20981  chfacfscmulgsum  21035  chfacfpmmulgsum  21039  ntrval  21211  clsval  21212  lpval  21314  1stcfb  21619  cnmpt11  21837  cnmpt21  21845  cnmptkp  21854  cnmptk1p  21859  iunmbl  23719  cnmptlimc  24053  limccnp  24054  limcco  24056  coe1termlem  24413  coe1term  24414  ulmval  24533  pserulm  24575  efgh  24687  rlimcnp  25105  xrlimcnp  25108  dchrelbasd  25377  gausslemma2dlem4  25507  2lgslem1b  25530  tgjustr  25786  midf  26085  ismidb  26087  lmif  26094  islmib  26096  wksfval  26907  crctcshwlkn0lem2  27110  crctcshwlkn0lem3  27111  wwlks  27134  wlkswwlksf1o  27178  clwwlk  27312  clwlkclwwlkf1  27347  spanval  28747  fzto1stfv1  30396  esumcvg  30693  omsval  30900  eulerpartlemgvv  30983  cndprobval  31041  reprval  31237  hgt750lemb  31283  climlec3  32161  madeval  32474  fwddifval  32808  knoppcnlem1  33016  knoppcnlem9  33024  unbdqndv2lem2  33033  knoppndvlem4  33038  knoppndvlem6  33040  heiborlem4  34155  heiborlem6  34157  pclvalN  35965  rabdiophlem2  38210  fphpdo  38225  monotoddzz  38351  dnnumch3lem  38459  pwssplit4  38502  hbtlem1  38536  rgspnval  38581  fvmptiunrelexplb0d  38817  fvmptiunrelexplb1d  38819  wessf1ornlem  40179  projf1o  40194  fmuldfeq  40610  clim1fr1  40628  mullimcf  40650  sumnnodd  40657  expfac  40684  fnlimfvre2  40704  fnlimabslt  40706  limsuplt2  40780  liminfval  40786  limsupge  40788  cncfshift  40882  cncfiooicclem1  40901  fprodsubrecnncnvlem  40916  fprodaddrecnncnvlem  40918  ioodvbdlimc1lem1  40941  ioodvbdlimc1lem2  40942  dvnmul  40953  dvnprodlem1  40956  dvnprodlem2  40957  dvnprodlem3  40958  itgsinexp  40965  stoweidlem7  41018  stoweidlem17  41028  stoweidlem26  41037  stoweidlem30  41041  stoweidlem31  41042  stoweidlem32  41043  stoweidlem34  41045  wallispilem4  41079  wallispi  41081  stirlinglem3  41087  stirlinglem5  41089  stirlinglem7  41091  stirlinglem10  41094  dirkercncflem2  41115  etransclem1  41246  etransclem27  41272  etransclem46  41291  etransclem48  41293  sge0snmptf  41445  nnfoctbdjlem  41463  psmeasurelem  41478  psmeasure  41479  meaiuninclem  41488  meaiininclem  41494  carageniuncllem1  41529  carageniuncllem2  41530  caratheodorylem1  41534  0ome  41537  ovnval2b  41560  hoiprodcl2  41563  ovnlecvr  41566  ovncvrrp  41572  ovnsubaddlem1  41578  hsphoif  41584  hoidmvval  41585  hsphoival  41587  ovnhoilem1  41609  hspval  41617  ovncvr2  41619  hspmbllem2  41635  ovnsubadd2lem  41653  vonioolem2  41689  vonicclem2  41692  issmflem  41730  smflimsuplem1  41820  smflimsuplem5  41824  smflimsuplem7  41826  fvmptrabdm  42196  prmdvdsfmtnof1  42329  upwlksfval  42563  sprsymrelfv  42591  lincop  43044  linc1  43061  lincext3  43092  el0ldep  43102  lincresunit2  43114  lincresunit3lem1  43115  digfval  43238  lines  43282  spheres  43298