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

Theorem fvmptd3 6789
Description: Deduction version of fvmpt 6767. (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 6765 . 2 ((𝐴𝐷𝐶𝑉) → (𝐹𝐴) = 𝐶)
61, 2, 5syl2anc 584 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  cmpt 5143  cfv 6354
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-iota 6313  df-fun 6356  df-fv 6362
This theorem is referenced by:  mptmpoopabbrd  7774  undefval  7938  tz7.44-2  8039  fvdiagfn  8449  resixpfo  8494  fival  8870  cantnfp1lem1  9135  cantnfp1lem2  9136  cantnfp1lem3  9137  wemapwe  9154  rankvalb  9220  djulcl  9333  djuss  9343  1stinl  9350  2ndinl  9351  1stinr  9352  2ndinr  9353  fin23lem27  9744  isf34lem1  9788  canthp1lem2  10069  wuncval  10158  climrlim2  14899  summolem3  15066  prodmolem3  15282  iprodmul  15352  lcmfval  15960  iserodd  16167  mreacs  16924  isofval  17022  isofn  17040  cicfval  17062  initoval  17252  termoval  17253  zerooval  17254  pwsco1mhm  17991  pwsco2mhm  17992  vrmdfval  18016  galactghm  18468  symgfixfolem1  18502  pmtrval  18515  pmtrfv  18516  pmtrdifwrdellem3  18547  gsummhm2  18995  gsummpt1n0  19021  dprdfid  19075  lspval  19683  aspval  20037  evlslem3  20228  coe1tmfv1  20377  coe1tmfv2  20378  uvcval  20864  mat1rhmval  21023  scmatrhmval  21071  marepvval  21111  mply1topmatval  21347  mp2pm2mplem1  21349  chfacfscmulgsum  21403  chfacfpmmulgsum  21407  tgval  21498  ntrval  21579  clsval  21580  opncldf2  21628  neival  21645  lpval  21682  1stcfb  21988  cnmpt11  22206  cnmpt21  22214  cnmptkp  22223  cnmptk1p  22228  ustval  22745  iunmbl  24088  cnmptlimc  24422  limccnp  24423  limcco  24425  coe1termlem  24782  coe1term  24783  ulmval  24902  pserulm  24944  efgh  25057  rlimcnp  25476  xrlimcnp  25479  dchrelbasd  25748  gausslemma2dlem4  25878  2lgslem1b  25901  tgjustr  26193  mirval  26374  midf  26495  ismidb  26497  lmif  26504  islmib  26506  wksfval  27324  crctcshwlkn0lem2  27522  crctcshwlkn0lem3  27523  wwlks  27546  wlkiswwlks2lem2  27581  wlkswwlksf1o  27590  clwwlk  27694  clwlkclwwlkf1  27721  numclwlk2lem2fv  28090  spanval  29043  fsuppcurry1  30393  fsuppcurry2  30394  fzto1stfv1  30676  tocycval  30683  prmidlval  30879  indv  31176  esumcvg  31250  omsval  31456  eulerpartlemgvv  31539  cndprobval  31596  reprval  31786  hgt750lemb  31832  satfvsuc  32511  sat1el2xp  32529  fmlasuc0  32534  climlec3  32868  madeval  33192  fwddifval  33526  knoppcnlem1  33735  knoppcnlem9  33743  unbdqndv2lem2  33752  knoppndvlem4  33757  knoppndvlem6  33759  bj-diagval  34364  heiborlem4  34979  heiborlem6  34981  pclvalN  36912  frlmsnic  39033  rabdiophlem2  39283  fphpdo  39298  monotoddzz  39424  dnnumch3lem  39530  pwssplit4  39573  hbtlem1  39607  rgspnval  39652  eliunov2  39908  fvmptiunrelexplb0d  39913  fvmptiunrelexplb1d  39915  dssmapfvd  40247  wessf1ornlem  41329  projf1o  41343  fmuldfeq  41748  clim1fr1  41766  mullimcf  41788  sumnnodd  41795  expfac  41822  fnlimfv  41828  fnlimfvre2  41842  fnlimabslt  41844  limsuplt2  41918  liminfval  41924  limsupge  41926  cncfshift  42041  cncfiooicclem1  42060  fprodsubrecnncnvlem  42075  fprodaddrecnncnvlem  42077  ioodvbdlimc1lem1  42100  ioodvbdlimc1lem2  42101  dvnmul  42112  dvnprodlem1  42115  dvnprodlem2  42116  dvnprodlem3  42117  itgsinexp  42124  stoweidlem7  42177  stoweidlem17  42187  stoweidlem26  42196  stoweidlem30  42200  stoweidlem31  42201  stoweidlem32  42202  stoweidlem34  42204  wallispilem4  42238  wallispi  42240  stirlinglem3  42246  stirlinglem5  42248  stirlinglem7  42250  stirlinglem10  42253  dirkercncflem2  42274  etransclem1  42405  etransclem12  42416  etransclem27  42431  etransclem46  42450  etransclem48  42452  sge0snmptf  42604  nnfoctbdjlem  42622  psmeasurelem  42637  psmeasure  42638  meaiuninclem  42647  meaiininclem  42653  carageniuncllem1  42688  carageniuncllem2  42689  caratheodorylem1  42693  0ome  42696  vonval  42707  ovnval  42708  ovnval2b  42719  hoiprodcl2  42722  ovnlecvr  42725  ovncvrrp  42731  ovnsubaddlem1  42737  hsphoif  42743  hoidmvval  42744  hsphoival  42746  ovnhoilem1  42768  hoidifhspval  42775  hspval  42776  ovncvr2  42778  hspmbllem2  42794  ovnsubadd2lem  42812  vonioolem2  42848  vonicclem2  42851  issmflem  42889  smflimsuplem1  42979  smflimsuplem5  42983  smflimsuplem7  42985  fvmptrabdm  43377  sprsymrelfv  43507  prproropf1olem4  43519  fmtno  43542  prmdvdsfmtnof1  43600  upwlksfval  43861  uspgrsprfv  43871  assintopval  44014  lincop  44365  linc1  44382  lincext3  44413  el0ldep  44423  lincresunit2  44435  lincresunit3lem1  44436  blenval  44533  digfval  44559  lines  44620  spheres  44635
  Copyright terms: Public domain W3C validator