Theorem fvmptd3 7043

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ↦ cmpt 5190  ‘cfv 6561

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-iota 6515  df-fun 6563  df-fv 6569

This theorem is used by:  mptmpoopabbrd  8122  undefval  8325  tz7.44-2  8446  fsetfocdm  8914  fvdiagfn  8950  resixpfo  8995  fival  9434  cantnfp1lem1  9709  cantnfp1lem2  9710  cantnfp1lem3  9711  wemapwe  9728  rankvalb  9835  djulcl  10021  djuss  10031  1stinl  10038  2ndinl  10039  1stinr  10040  2ndinr  10041  fin23lem27  10436  isf34lem1  10480  canthp1lem2  10768  wuncval  10857  indv  12352  climrlim2  15746  summolem3  15912  prodmolem3  16132  iprodmul  16202  lcmfval  16828  iserodd  17045  mreacs  17864  isofval  17964  isofn  17982  cicfval  18004  initoval  18200  termoval  18201  zerooval  18202  pwsco1mhm  19060  pwsco2mhm  19061  vrmdfval  19084  ghmqusnsglem1  19527  ghmquskerlem1  19530  galactghm  19651  symgfixfolem1  19685  pmtrval  19698  pmtrfv  19699  pmtrdifwrdellem3  19730  gsummhm2  20186  gsummpt1n0  20212  dprdfid  20266  rgspnval  20897  lspval  21283  prmidlval  21651  uvcval  22124  aspval  22213  evlslem3  22422  evlsvvval  22435  mplmapghm  22464  evlsmaprhm  22473  evlsevl  22474  selvvvval  22484  psdmplcl  22516  psdadd  22517  psdmul  22520  psdmvr  22523  coe1tmfv1  22626  coe1tmfv2  22627  evls1maprhm  22727  evls1maplmhm  22728  rhmmpl  22731  rhmply1vr1  22735  rhmply1vsca  22736  mat1rhmval  22827  scmatrhmval  22875  marepvval  22915  mply1topmatval  23155  mp2pm2mplem1  23157  chfacfscmulgsum  23211  chfacfpmmulgsum  23215  tgval  23306  ntrval  23387  clsval  23388  opncldf2  23436  neival  23453  lpval  23490  1stcfb  23796  cnmpt11  24015  cnmpt21  24023  cnmptkp  24032  cnmptk1p  24037  ustval  24555  iunmbl  25907  cnmptlimc  26243  limccnp  26244  limcco  26246  coe1termlem  26610  coe1term  26611  ulmval  26740  pserulm  26782  efgh  26902  rlimcnp  27326  xrlimcnp  27329  dchrelbasd  27599  gausslemma2dlem4  27729  2lgslem1b  27752  madeval  28251  abssval  28658  tgjustr  28969  mirval  29160  tgplnfn  29286  plngval  29288  isplng  29289  midf  29314  ismidb  29316  lmif  29323  islmib  29325  cgrabasimass  29411  angmgmval  29427  brprlng  29449  wksfval  30223  crctcshwlkn0lem2  30433  crctcshwlkn0lem3  30434  wwlks  30457  wlkiswwlks2lem2  30492  wlkswwlksf1o  30501  clwwlk  30607  clwlkclwwlkf1  30634  numclwlk2lem2fv  31012  spanval  31968  fsuppcurry1  33389  fsuppcurry2  33390  mndlactf1  33663  mndlactfo  33664  mndractf1  33665  mndractfo  33666  mndlactf1o  33667  mndractf1o  33668  gsummulsubdishift1s  33707  gsummulsubdishift2s  33708  gsumwrd2dccat  33715  fzto1stfv1  33738  tocycval  33745  fxpsubm  33809  fxpsubg  33810  fxpsubrg  33811  fxpsdrg  33812  elrgspnlem1  33879  elrgspnlem2  33880  elrgspnsubrunlem2  33885  rlocf1  33911  qusrn  34044  elrspunidl  34062  elrspunsn  34063  rprmval  34132  zringfrac  34169  ply1gsumz  34214  r1plmhm  34224  0mplrim  34229  selvply1rhmlema  34233  selvply1rhmlemb  34234  selvply1rhmlem3  34237  selvply1rhmlem5  34239  extvfvcl  34251  mplvrpmrhm  34262  psrmonmul2  34266  psrmonprod  34267  esplyfvaln  34289  vietadeg1  34293  ply1degltdimlem  34337  lactlmhm  34349  evls1fldgencl  34385  fldextrspunlsplem  34388  fldextrspunlsp  34389  ply1annidllem  34416  algextdeglem7  34438  rhmpreimacnlem  34599  esumcvg  34801  omsval  35008  eulerpartlemgvv  35091  cndprobval  35148  reprval  35322  hgt750lemb  35368  fineqvnttrclselem2  35903  fineqvnttrclselem3  35904  fineqvnttrclse  35905  satfvsuc  36306  sat1el2xp  36324  fmlasuc0  36329  climlec3  36690  fwddifval  37118  knoppcnlem1  37550  knoppcnlem9  37558  unbdqndv2lem2  37567  knoppndvlem4  37572  knoppndvlem6  37574  bj-diagval  38300  bj-endval  38441  heiborlem4  38951  heiborlem6  38953  pclvalN  41150  frlmsnic  43808  rhmpsr  43815  evlsbagval  43818  evlselv  43821  mhphflem  43828  frlmnzcoordval  43857  prjspnnormval  43863  rabdiophlem2  44013  fphpdo  44028  monotoddzz  44154  dnnumch3lem  44257  pwssplit4  44295  hbtlem1  44328  eliunov2  44882  fvmptiunrelexplb0d  44887  fvmptiunrelexplb1d  44889  dssmapfvd  45220  wessf1ornlem  46415  projf1o  46426  fmuldfeq  46810  clim1fr1  46828  mullimcf  46850  sumnnodd  46857  expfac  46882  fnlimfv  46888  fnlimfvre2  46902  fnlimabslt  46904  limsuplt2  46978  liminfval  46984  limsupge  46986  cncfshift  47099  cncfiooicclem1  47118  fprodsubrecnncnvlem  47132  fprodaddrecnncnvlem  47134  ioodvbdlimc1lem1  47156  ioodvbdlimc1lem2  47157  dvnmul  47168  dvnprodlem1  47171  dvnprodlem2  47172  dvnprodlem3  47173  itgsinexp  47180  stoweidlem7  47232  stoweidlem17  47242  stoweidlem26  47251  stoweidlem30  47255  stoweidlem31  47256  stoweidlem32  47257  stoweidlem34  47259  wallispilem4  47293  wallispi  47295  stirlinglem3  47301  stirlinglem5  47303  stirlinglem7  47305  stirlinglem10  47308  dirkercncflem2  47329  fourierdlem48  47379  fourierdlem49  47380  etransclem1  47460  etransclem12  47471  etransclem27  47486  etransclem46  47505  etransclem48  47507  sge0snmptf  47662  nnfoctbdjlem  47680  psmeasurelem  47695  psmeasure  47696  meaiuninclem  47705  meaiininclem  47711  carageniuncllem1  47746  carageniuncllem2  47747  caratheodorylem1  47751  0ome  47754  vonval  47765  ovnval  47766  ovnval2b  47777  hoiprodcl2  47780  ovnlecvr  47783  ovncvrrp  47789  ovnsubaddlem1  47795  hsphoif  47801  hoidmvval  47802  hsphoival  47804  ovnhoilem1  47826  hoidifhspval  47833  hspval  47834  ovncvr2  47836  hspmbllem2  47852  ovnsubadd2lem  47870  vonioolem2  47906  vonicclem2  47909  issmflem  47952  smflimsuplem1  48045  smflimsuplem5  48049  smflimsuplem7  48051  tmachlem-tpitem  48165  fvmptrabdm  48578  sprsymrelfv  48791  prproropf1olem4  48803  fmtno  48829  prmdvdsfmtnof1  48887  ppivalnn  48932  upwlksfval  49448  uspgrsprfv  49458  assintopval  49517  lincop  49735  linc1  49752  lincext3  49783  el0ldep  49793  lincresunit2  49805  lincresunit3lem1  49806  blenval  49898  digfval  49924  itcoval  49988  ackval0012  50016  ackval1012  50017  ackval2012  50018  ackval3012  50019  lines  50059  spheres  50073  invfn  50359  fucoid  50685  crosspdot0lem  51275  crosspaltd  51278  crossp3d  51279  veroquadgsumlem  51295  veroquadmodzerod  51296