Theorem fvmptd3 7009

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186  ‘cfv 6531

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539

This theorem is used by:  mptmpoopabbrd  8083  undefval  8278  tz7.44-2  8399  fsetfocdm  8867  fvdiagfn  8903  resixpfo  8948  fival  9388  cantnfp1lem1  9663  cantnfp1lem2  9664  cantnfp1lem3  9665  wemapwe  9682  rankvalb  9787  djulcl  9972  djuss  9982  1stinl  9989  2ndinl  9990  1stinr  9991  2ndinr  9992  fin23lem27  10387  isf34lem1  10431  canthp1lem2  10719  wuncval  10808  indv  12303  climrlim2  15694  summolem3  15860  prodmolem3  16080  iprodmul  16150  lcmfval  16776  iserodd  16993  mreacs  17812  isofval  17912  isofn  17930  cicfval  17952  initoval  18148  termoval  18149  zerooval  18150  pwsco1mhm  19008  pwsco2mhm  19009  vrmdfval  19032  ghmqusnsglem1  19474  ghmquskerlem1  19477  galactghm  19598  symgfixfolem1  19632  pmtrval  19645  pmtrfv  19646  pmtrdifwrdellem3  19677  gsummhm2  20133  gsummpt1n0  20159  dprdfid  20213  rgspnval  20844  lspval  21230  prmidlval  21598  uvcval  22071  aspval  22160  evlslem3  22369  evlsvvval  22382  mplmapghm  22411  evlsmaprhm  22420  evlsevl  22421  selvvvval  22431  psdmplcl  22463  psdadd  22464  psdmul  22467  psdmvr  22470  coe1tmfv1  22573  coe1tmfv2  22574  evls1maprhm  22674  evls1maplmhm  22675  rhmmpl  22678  rhmply1vr1  22682  rhmply1vsca  22683  mat1rhmval  22774  scmatrhmval  22822  marepvval  22862  mply1topmatval  23102  mp2pm2mplem1  23104  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  tgval  23253  ntrval  23334  clsval  23335  opncldf2  23383  neival  23400  lpval  23437  1stcfb  23743  cnmpt11  23962  cnmpt21  23970  cnmptkp  23979  cnmptk1p  23984  ustval  24502  iunmbl  25854  cnmptlimc  26190  limccnp  26191  limcco  26193  coe1termlem  26557  coe1term  26558  ulmval  26689  pserulm  26731  efgh  26851  rlimcnp  27275  xrlimcnp  27278  dchrelbasd  27548  gausslemma2dlem4  27678  2lgslem1b  27701  madeval  28200  abssval  28607  tgjustr  28918  mirval  29109  tgplnfn  29235  plngval  29237  isplng  29238  midf  29263  ismidb  29265  lmif  29272  islmib  29274  cgrabasimass  29360  angmgmval  29376  brprlng  29398  wksfval  30172  crctcshwlkn0lem2  30382  crctcshwlkn0lem3  30383  wwlks  30406  wlkiswwlks2lem2  30441  wlkswwlksf1o  30450  clwwlk  30556  clwlkclwwlkf1  30583  numclwlk2lem2fv  30961  spanval  31917  fsuppcurry1  33298  fsuppcurry2  33299  mndlactf1  33569  mndlactfo  33570  mndractf1  33571  mndractfo  33572  mndlactf1o  33573  mndractf1o  33574  gsummulsubdishift1s  33613  gsummulsubdishift2s  33614  gsumwrd2dccat  33621  fzto1stfv1  33644  tocycval  33651  fxpsubm  33715  fxpsubg  33716  fxpsubrg  33717  fxpsdrg  33718  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnsubrunlem2  33791  rlocf1  33817  qusrn  33942  elrspunidl  33960  elrspunsn  33961  rprmval  34030  zringfrac  34068  ply1gsumz  34113  r1plmhm  34123  0mplrim  34128  selvply1rhmlema  34132  selvply1rhmlemb  34133  selvply1rhmlem3  34136  selvply1rhmlem5  34138  extvfvcl  34150  mplvrpmrhm  34161  psrmonmul2  34165  psrmonprod  34166  esplyfvaln  34188  vietadeg1  34192  ply1degltdimlem  34236  lactlmhm  34248  evls1fldgencl  34284  fldextrspunlsplem  34287  fldextrspunlsp  34288  ply1annidllem  34315  algextdeglem7  34337  rhmpreimacnlem  34498  esumcvg  34700  omsval  34908  eulerpartlemgvv  34991  cndprobval  35048  reprval  35222  hgt750lemb  35268  fineqvnttrclselem2  35763  fineqvnttrclselem3  35764  fineqvnttrclse  35765  satfvsuc  36095  sat1el2xp  36113  fmlasuc0  36118  climlec3  36468  fwddifval  36897  knoppcnlem1  37329  knoppcnlem9  37337  unbdqndv2lem2  37346  knoppndvlem4  37351  knoppndvlem6  37353  bj-diagval  38063  bj-endval  38204  heiborlem4  38716  heiborlem6  38718  pclvalN  40915  frlmsnic  43566  rhmpsr  43573  evlsbagval  43576  evlselv  43579  mhphflem  43586  prjspnfv01  43614  prjspner01  43615  prjspner1  43616  rabdiophlem2  43762  fphpdo  43777  monotoddzz  43903  dnnumch3lem  44006  pwssplit4  44049  hbtlem1  44083  eliunov2  44638  fvmptiunrelexplb0d  44643  fvmptiunrelexplb1d  44645  dssmapfvd  44976  wessf1ornlem  46143  projf1o  46154  fmuldfeq  46539  clim1fr1  46557  mullimcf  46579  sumnnodd  46586  expfac  46611  fnlimfv  46617  fnlimfvre2  46631  fnlimabslt  46633  limsuplt2  46707  liminfval  46713  limsupge  46715  cncfshift  46828  cncfiooicclem1  46847  fprodsubrecnncnvlem  46861  fprodaddrecnncnvlem  46863  ioodvbdlimc1lem1  46885  ioodvbdlimc1lem2  46886  dvnmul  46897  dvnprodlem1  46900  dvnprodlem2  46901  dvnprodlem3  46902  itgsinexp  46909  stoweidlem7  46961  stoweidlem17  46971  stoweidlem26  46980  stoweidlem30  46984  stoweidlem31  46985  stoweidlem32  46986  stoweidlem34  46988  wallispilem4  47022  wallispi  47024  stirlinglem3  47030  stirlinglem5  47032  stirlinglem7  47034  stirlinglem10  47037  dirkercncflem2  47058  fourierdlem48  47108  fourierdlem49  47109  etransclem1  47189  etransclem12  47200  etransclem27  47215  etransclem46  47234  etransclem48  47236  sge0snmptf  47391  nnfoctbdjlem  47409  psmeasurelem  47424  psmeasure  47425  meaiuninclem  47434  meaiininclem  47440  carageniuncllem1  47475  carageniuncllem2  47476  caratheodorylem1  47480  0ome  47483  vonval  47494  ovnval  47495  ovnval2b  47506  hoiprodcl2  47509  ovnlecvr  47512  ovncvrrp  47518  ovnsubaddlem1  47524  hsphoif  47530  hoidmvval  47531  hsphoival  47533  ovnhoilem1  47555  hoidifhspval  47562  hspval  47563  ovncvr2  47565  hspmbllem2  47581  ovnsubadd2lem  47599  vonioolem2  47635  vonicclem2  47638  issmflem  47681  smflimsuplem1  47774  smflimsuplem5  47778  smflimsuplem7  47780  tmachlem-tpitem  47894  fvmptrabdm  48307  sprsymrelfv  48520  prproropf1olem4  48532  fmtno  48558  prmdvdsfmtnof1  48616  ppivalnn  48661  upwlksfval  49177  uspgrsprfv  49187  assintopval  49246  lincop  49464  linc1  49481  lincext3  49512  el0ldep  49522  lincresunit2  49534  lincresunit3lem1  49535  blenval  49627  digfval  49653  itcoval  49717  ackval0012  49745  ackval1012  49746  ackval2012  49747  ackval3012  49748  lines  49787  spheres  49802  invfn  50082  fucoid  50400  crosspdot0lem  50907  crosspaltd  50910  crossp3d  50911  veroquadgsumlem  50927  veroquadmodzerod  50928