MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmptd3 Structured version   Visualization version   GIF version

Theorem fvmptd3 6783
Description: Deduction version of fvmpt 6761. (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
StepHypRef Expression
1 fvmptd3.3 . 2 (𝜑𝐴𝐷)
2 fvmptd3.4 . 2 (𝜑𝐶𝑉)
3 fvmptd3.2 . . 3 (𝑥 = 𝐴𝐵 = 𝐶)
4 fvmptd3.1 . . 3 𝐹 = (𝑥𝐷𝐵)
53, 4fvmptg 6759 . 2 ((𝐴𝐷𝐶𝑉) → (𝐹𝐴) = 𝐶)
61, 2, 5syl2anc 584 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  cmpt 5137  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356
This theorem is referenced by:  mptmpoopabbrd  7767  undefval  7931  tz7.44-2  8032  fvdiagfn  8443  resixpfo  8488  fival  8864  cantnfp1lem1  9129  cantnfp1lem2  9130  cantnfp1lem3  9131  wemapwe  9148  rankvalb  9214  djulcl  9327  djuss  9337  1stinl  9344  2ndinl  9345  1stinr  9346  2ndinr  9347  fin23lem27  9738  isf34lem1  9782  canthp1lem2  10063  wuncval  10152  climrlim2  14892  summolem3  15059  prodmolem3  15275  iprodmul  15345  lcmfval  15953  iserodd  16160  mreacs  16917  isofval  17015  isofn  17033  cicfval  17055  initoval  17245  termoval  17246  zerooval  17247  pwsco1mhm  17984  pwsco2mhm  17985  vrmdfval  18009  galactghm  18461  symgfixfolem1  18495  pmtrval  18508  pmtrfv  18509  pmtrdifwrdellem3  18540  gsummhm2  18988  gsummpt1n0  19014  dprdfid  19068  lspval  19676  aspval  20030  evlslem3  20221  coe1tmfv1  20370  coe1tmfv2  20371  uvcval  20857  mat1rhmval  21016  scmatrhmval  21064  marepvval  21104  mply1topmatval  21340  mp2pm2mplem1  21342  chfacfscmulgsum  21396  chfacfpmmulgsum  21400  tgval  21491  ntrval  21572  clsval  21573  opncldf2  21621  neival  21638  lpval  21675  1stcfb  21981  cnmpt11  22199  cnmpt21  22207  cnmptkp  22216  cnmptk1p  22221  ustval  22738  iunmbl  24081  cnmptlimc  24415  limccnp  24416  limcco  24418  coe1termlem  24775  coe1term  24776  ulmval  24895  pserulm  24937  efgh  25052  rlimcnp  25470  xrlimcnp  25473  dchrelbasd  25742  gausslemma2dlem4  25872  2lgslem1b  25895  tgjustr  26187  mirval  26368  midf  26489  ismidb  26491  lmif  26498  islmib  26500  wksfval  27318  crctcshwlkn0lem2  27516  crctcshwlkn0lem3  27517  wwlks  27540  wlkiswwlks2lem2  27575  wlkswwlksf1o  27584  clwwlk  27688  clwlkclwwlkf1  27715  numclwlk2lem2fv  28084  spanval  29037  fsuppcurry1  30387  fsuppcurry2  30388  fzto1stfv1  30670  tocycval  30677  prmidlval  30873  indv  31170  esumcvg  31244  omsval  31450  eulerpartlemgvv  31533  cndprobval  31590  reprval  31780  hgt750lemb  31826  satfvsuc  32505  sat1el2xp  32523  fmlasuc0  32528  climlec3  32862  madeval  33186  fwddifval  33520  knoppcnlem1  33729  knoppcnlem9  33737  unbdqndv2lem2  33746  knoppndvlem4  33751  knoppndvlem6  33753  bj-diagval  34358  heiborlem4  34973  heiborlem6  34975  pclvalN  36906  frlmsnic  39027  rabdiophlem2  39277  fphpdo  39292  monotoddzz  39418  dnnumch3lem  39524  pwssplit4  39567  hbtlem1  39601  rgspnval  39646  eliunov2  39902  fvmptiunrelexplb0d  39907  fvmptiunrelexplb1d  39909  dssmapfvd  40241  wessf1ornlem  41321  projf1o  41335  fmuldfeq  41740  clim1fr1  41758  mullimcf  41780  sumnnodd  41787  expfac  41814  fnlimfv  41820  fnlimfvre2  41834  fnlimabslt  41836  limsuplt2  41910  liminfval  41916  limsupge  41918  cncfshift  42033  cncfiooicclem1  42052  fprodsubrecnncnvlem  42067  fprodaddrecnncnvlem  42069  ioodvbdlimc1lem1  42092  ioodvbdlimc1lem2  42093  dvnmul  42104  dvnprodlem1  42107  dvnprodlem2  42108  dvnprodlem3  42109  itgsinexp  42116  stoweidlem7  42169  stoweidlem17  42179  stoweidlem26  42188  stoweidlem30  42192  stoweidlem31  42193  stoweidlem32  42194  stoweidlem34  42196  wallispilem4  42230  wallispi  42232  stirlinglem3  42238  stirlinglem5  42240  stirlinglem7  42242  stirlinglem10  42245  dirkercncflem2  42266  etransclem1  42397  etransclem12  42408  etransclem27  42423  etransclem46  42442  etransclem48  42444  sge0snmptf  42596  nnfoctbdjlem  42614  psmeasurelem  42629  psmeasure  42630  meaiuninclem  42639  meaiininclem  42645  carageniuncllem1  42680  carageniuncllem2  42681  caratheodorylem1  42685  0ome  42688  vonval  42699  ovnval  42700  ovnval2b  42711  hoiprodcl2  42714  ovnlecvr  42717  ovncvrrp  42723  ovnsubaddlem1  42729  hsphoif  42735  hoidmvval  42736  hsphoival  42738  ovnhoilem1  42760  hoidifhspval  42767  hspval  42768  ovncvr2  42770  hspmbllem2  42786  ovnsubadd2lem  42804  vonioolem2  42840  vonicclem2  42843  issmflem  42881  smflimsuplem1  42971  smflimsuplem5  42975  smflimsuplem7  42977  fvmptrabdm  43369  sprsymrelfv  43533  prproropf1olem4  43545  fmtno  43568  prmdvdsfmtnof1  43626  upwlksfval  43887  uspgrsprfv  43897  assintopval  44040  lincop  44391  linc1  44408  lincext3  44439  el0ldep  44449  lincresunit2  44461  lincresunit3lem1  44462  blenval  44559  digfval  44585  lines  44646  spheres  44661
  Copyright terms: Public domain W3C validator